Researcher profile

Jianlin Wang

Jianlin Wang contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 19 - UnverifiedVerification L1Unclaimed author
5works
0followers
4topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

5 published item(s)

preprint2026arXiv

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberger (WZ) method can achieve a mechanized proof of combinatorial identities by constructing special auxiliary functions and demonstrating that they satisfy specific recurrence relations. We propose WZ-LLM, a neuro-symbolic framework that turns WZ proof plans into executable proof sketches in Lean 4 and uses an LLM-based prover to discharge the resulting machine-checkable subgoals. We also train a dedicated WZ-Prover via a Lean-kernel-verified bootstrapping loop with expert-verified iteration, followed by DAPO-based refinement. Experiments show that WZ-LLM achieves a 34% proof success rate on LCI-Test (100 classic combinatorial identities), outperforming strong baselines such as DeepSeek-V3 and Goedel-Prover-V2, and delivering consistent gains on CombiBench and PutnamBench-Comb. These results indicate that our framework provides two complementary strengths: improved direct proving for identities beyond the scope of WZ, and substantially higher end-to-end success when WZ sketches guide a specialized prover.

preprint2026arXiv

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.

preprint2022arXiv

DC-SPP-YOLO: Dense Connection and Spatial Pyramid Pooling Based YOLO for Object Detection

Although the YOLOv2 method is extremely fast on object detection, its detection accuracy is restricted due to the low performance of its backbone network and the underutilization of multi-scale region features. Therefore, a dense connection (DC) and spatial pyramid pooling (SPP) based YOLO (DC-SPP-YOLO) method for ameliorating the object detection accuracy of YOLOv2 is proposed in this paper. Specifically, the dense connection of convolution layers is employed in the backbone network of YOLOv2 to strengthen the feature extraction and alleviate the vanishing-gradient problem. Moreover, an improved spatial pyramid pooling is introduced to pool and concatenate the multi-scale region features, so that the network can learn the object features more comprehensively. The DC-SPP-YOLO model is established and trained based on a new loss function composed of MSE (mean square error) loss and cross-entropy loss. The experimental results indicated that the mAP (mean Average Precision) of DC-SPP-YOLO is higher than that of YOLOv2 on the PASCAL VOC datasets and the UA-DETRAC datasets. The effectiveness of DC-SPP-YOLO method proposed is demonstrated.

preprint2021arXiv

Spin-glass state induced by Mn-doping into a moderate gap layered semiconductor SnSe$_2$

Various types of magnetism can appear in emerging quantum materials such as van der Waals layered ones. Here, we report the successful doping of manganese atoms into a post-transition metal dichalcogenide semiconductor: SnSe$_2$. We synthesized a single crystal Sn$_{1-x}$Mn$_x$Se$_{2}$ with $\textit{x}$ = 0.04 by the chemical vapor transport (CVT) method and characterized it by x-ray diffraction (XRD) and energy-dispersive x-ray spectroscopy (EDS). The magnetic properties indicated a competition between coexisting ferromagnetic and antiferromagnetic interactions, from the temperature dependence of the magnetization, together with magnetic hysteresis loops. This means that magnetic clusters having ferromagnetic interaction within a cluster form and the short-range antiferromagnetic interaction works between the clusters; a spin-glass state appears below ~ 60 K. Furthermore, we confirmed by $\textit{ab initio}$ calculations that the ferromagnetic interaction comes from the 3$\textit{d}$ electrons of the manganese dopant. Our results offer a new material platform to understand and utilize the magnetism in the van der Waals layered materials.

preprint2020arXiv

Fermi liquid behavior and colossal magnetoresistance in layered MoOCl2

A characteristic of a Fermi liquid is the T^2 dependence of its resistivity, sometimes referred to as the Baber law. However, for most metals, this behavior is only restricted to very low temperatures, usually below 20 K. Here, we experimentally demonstrate that for the single-crystal van der Waals layered material MoOCl2, the Baber law holds in a wide temperature range up to ~120 K, indicating that the electron-electron scattering plays a dominant role in this material. Combining with the specific heat measurement, we find that the modified Kadowaki-Woods ratio of the material agrees well with many other strongly correlated metals. Furthermore, in the magneto-transport measurement, a colossal magneto-resistance is observed, which reaches ~350% at 9 T and displays no sign of saturation. With the help of first-principles calculations, we attribute this behavior to the presence of open orbits on the Fermi surface. We also suggest that the dominance of electron-electron scattering is related to an incipient charge density wave state of the material. Our results establish MoOCl2 as a strongly correlated metal and shed light on the underlying physical mechanism, which may open a new path for exploring the effects of electron-electron interaction in van der Waals layered structures.