AI Proof Bridge

Inspiration

We are developing NPA, Nano Proof Auditor, an AI-native theorem prover designed for large-scale formal mathematics.

However, every new proof system faces an important question:

How can mathematicians trust the proofs it generates?

A proof may be formally checked inside a new system, but trust also depends on interoperability with established tools. We wanted NPA proofs to be independently verifiable using Lean, one of the most widely trusted proof assistants in the mathematical community.

This inspired us to build NPA Lean Exporter: a bridge between AI-native theorem proving and Lean’s trusted kernel.

What it does

NPA Lean Exporter translates checked and certified NPA proof packages into Lean declarations.

The generated Lean code can then be checked independently by Lean, allowing users to verify NPA proofs without trusting the exporter or the NPA implementation as part of the final verification boundary.

For example, this NPA theorem:

theorem id :
  forall (A : Type), forall (x : A), A :=
  fun A => fun x => x

is exported as a Lean declaration equivalent to:

opaque NpaExport.Pkg_npa_proof_corpus_v0_1_0.Proofs_Ai_Basic.id :
  ((x0 : (Sort (0 + 1))) -> ((x1 : x0) -> x0)) :=
  (fun (x0 : (Sort (0 + 1))) => (fun (x1 : x0) => x1))

Lean’s kernel can independently type-check the exported declaration.

By connecting NPA with Lean, the exporter makes AI-generated formal mathematics easier to verify, share, review, and build upon.

How we built it

We built the exporter with Codex and GPT-5.6 basically in a day.

The project includes:

• Translation from certified NPA terms and declarations into Lean syntax
• Translation of universes, dependent function types, lambdas, applications, and constants
• Validation of exported output using a real Lean toolchain
• Automated tests covering successful exports and unsupported or invalid inputs
• Command-line tooling for integration into development workflows
• Documentation

Codex helped us inspect the existing proof infrastructure, implement translation rules, generate tests, investigate failures, and rapidly iterate on the exporter’s design. It also helped us improve documentation and verify that the documented Lean output matched the actual generated output.

Real-world demonstration

To evaluate the exporter beyond small examples, we integrated it into our ongoing formalization of Fermat’s Last Theorem in NPA.

The FLT formalization itself began before this hackathon. We checked AI generated NPA proofs using the newly developed exporter.

This gave us a realistic test case involving a large formal mathematics project—not only isolated demonstration theorems.

Challenges we faced

We faced little challenges because Codex did the job very well. We iterated several times to make the translated Lean code valid.

What we learned

A new theorem prover NPA was also develped using Codex, and it worked very well because proofs accepted in NPA also accepted in Lean by exporting them.

Accomplishments that we are proud of

• Built a practical bridge from NPA to Lean in a short period
• Exported certified AI-generated proofs into independently checkable Lean code
• Validated generated output with a real Lean toolchain
• Added deterministic behavior and extensive automated testing
• Applied the exporter to an ongoing large-scale formalization project
• Created an open-source developer tool that others can inspect and build upon

What’s next

We plan to speed up the exporter and proceed to use NPA and Codex to prove many difficult math problems, even open problems.

Our long-term vision is a future where AI helps mathematicians discover and construct new mathematics, while trusted proof assistants independently verify every result.

Built With

• codex
• formalverification
• gpt-5.6
• lean
• mathematics
• npa
• openai
• rust
• theoremproving