Inspiration
AI-generated mathematical proofs can look convincing while containing subtle errors. For someone learning formal mathematics, another challenge is turning an informal argument into code that a proof assistant can actually check.
I built LeanBridge AI to connect these two worlds: let a language model propose a formalization, then make the code and compiler feedback visible so users can inspect, edit, and verify it.
What it does
LeanBridge AI is a browser-based workbench that turns mathematical text or LaTeX into editable Lean 4 code.
NVIDIA Nemotron, served through Nebius Token Factory, generates the formalization. A real Lean 4 compiler with mathlib checks the result. If compilation fails, the application can send the actual diagnostics back to the model for a bounded repair attempt.
Users can inspect the generated theorem, edit its proof, run Lean again without another model request, and download the source as a .lean file. The workbench displays the verification status, compiler diagnostics, and attempt count.
How I built it
The application uses TypeScript, React, and Express. Separate components handle model requests, proof jobs, and Lean verification.
The demonstrated model is nvidia/nemotron-3-super-120b-a12b, accessed through Nebius Token Factory. Hosted inference lets the application use Nemotron without requiring a local GPU.
The backend runs alongside a pinned Lean/mathlib environment in Docker. Provider credentials stay on the server, while browser access uses a separate password and revocable sessions. Model requests, compiler execution, and automatic repair attempts have explicit limits.
I also added a Windows preflight launcher that checks configuration, Docker, and service readiness without making inference requests.
Challenges I ran into
One important challenge was distinguishing a mathematical error from an infrastructure failure. A compiler timeout should not trigger an unnecessary model repair request, and it must never be presented as a successful proof.
Another challenge was model output budgeting. During testing, reasoning consumed the completion budget without producing the expected final JSON. I added explicit handling for truncated responses and adjusted the bounded output budget.
Lean library names also proved difficult for the model. The real demonstration shows why compiler feedback matters: the first proposal used an unavailable add_comm identifier. Lean rejected it, and Nemotron repaired the code to use Nat.add_comm.
Accomplishments I'm proud of
The final demonstration records actual operation of the website, including:
- Entering a mathematical statement and generating Lean code.
- A real compiler rejection followed by an automatic repair that passes.
- Manually introducing a false theorem and seeing Lean reject it.
- Restoring the generated proof and successfully verifying it again.
- Downloading a source file that matches the editor.
The release has also passed 117 automated tests, 13 live HTTP and access-control checks, and CI checks for types and production builds.
What I learned
A useful AI mathematics tool needs more than plausible answers. It needs independent verification, clear failure states, and a workflow that keeps the user involved.
I also learned that successful compilation and faithful translation are separate questions. Lean checks the formal theorem, but a person must still confirm that this theorem expresses the intended mathematics.
What's next for LeanBridge AI
I want to improve mathlib name grounding, expand the evaluation set beyond simple examples, and measure semantic faithfulness, verification latency, and repair success separately.
The goal is to make formal verification more approachable while keeping its results inspectable.
Existing project and hackathon contributions
LeanBridge existed before this hackathon. During the submission period, I extended it with the Nebius Token Factory integration and NVIDIA Nemotron workflow, strengthened configuration and credential handling, added authenticated browser access and Windows preflight tooling, improved compiler diagnostics and bounded repair behavior, and validated the complete workflow with real model calls and Lean compilation.
Log in or sign up for Devpost to join the conversation.