Lean-based · Formal verification for research mathematics

Research papers, rebuilt as verifiable mathematics using AI.

LeanNexus formalizes research mathematics into machine-checked, Lean-based proofs — verifying every reasoning step, re-deriving every computation, and localizing the exact line where an argument breaks.

Request a pilot → View a verification run ↓

—Papers in the Public Library

—Published checkpoints

—Mapped proof nodes

Scroll

Producing advanced and verifiable mathematical data.

Three capabilities that turn expert reasoning into verified, reusable mathematical data.

Formalizing research mathematics is possible by domain experts, but it is slow, specialized, and difficult to scale. LeanNexus turns domain expertise into Lean automation to structure arguments, verify dependencies, re-derive key computations, and preserve the results as machine-checkable mathematical knowledge.

01 / Verification

Reasoning-chain verification

Each lemma, proposition and its dependency edges are formalized and discharged by the Lean kernel.

theorem graph 6 / 6 checked

02 / Computation

Numerical re-derivation

Constants, bounds and closed forms are re-computed from first principles with interval arithmetic and certified numerics.

certified trace interval.arith

Inputβ = 0.40 · √(2π)

DerivedI(β) ∈ [0.7318419, 0.7318421]

Error|ε| ≤ 2.1 × 10⁻⁷

kernel-checkable certificate emitted

03 / Debugging

Proof debugging & counterexamples

When a step goes wrong, we report the failing goal, the missing hypothesis, and where possible a concrete counterexample.

× unresolved goal 1 failure

have h_bound : ‖x − x⋆‖ ≤ ε := by
  apply norm_le_of_sq_le_sq
  exact bound_from_lemma h
end

⊢missing hypothesis: 0 < εpaper.tex:184

Proof artifacts that can be used for multiple purposes.

The output is not a report — it is a Lean repository plus an auditable dependency graph that anyone can re-check for their own purposes.

Stage 01

Submit

Upload a LaTeX project, point at an arXiv ID, or drop a single source file. Figures, .sty and .bib come along; version-control metadata is stripped.

Stage 02

Processing

The paper is decomposed into statements, definitions, and dependencies, then formalized in Lean against Mathlib. Every accepted step is checked by the Lean kernel.

Stage 03

Certificate

The output includes an interactive checkpoint graph, a Lean repository that builds from scratch, a structured categorization of each proof step, and clear recommendations for improving the argument.

The verification graph is the deliverable.

Select any node to trace a claim from the paper to its Lean statement, proof dependencies, and kernel status. The graph reveals what has been verified, what remains open, and exactly where a proof fails.

Online Stochastic Matching:Online Actions Based on Offline Statistics Source · arXiv 1007.1673v2 ↗ 35 outcome objects · 13 clusters · kernel green

Selected object

Proposition 2.1

Verified

The optimum vector f is a fractional matching, with $f_s \le r_s \le 1$ , and the edge bound $f_e \le 1-e^{-r_s}+o(1/b)$ .

ClusterFractional matching

Depends on3 objects

Work items8 · 8 closed

-- placeholder Lean
theorem opt_is_fractional_matching
    (G : BipartiteGraph) (f : EdgeVec G) :
    IsFractionalMatching f := by
  intro s hs
  simpa [edge_bound] using le_one_of_opt f s hs

Now in limited preview

Bring us the hardest section of your paper.

Start with one consequential section. We will return a verification graph, a Lean repository, and an honest list of what we could not close.

Request a pilot → View a verification run ↗