projects

autoformalization

These are my projects related to autoformalization and autoreasoning in Lean. Autoformalization refers to the process of translating mathematical statements and proofs into a formal language such as Lean, whereas autoreasoning denotes the ability of a system to produce original formal proofs with minimal human intervention.

Among other motivations, the most ambitious possible outcome of this work would be a system capable of producing novel mathematical results, which, having been written in a formal language, would be a priori correct.

neumann-prover

An end-to-end, multi-purpose Lean autoformalization and autoreasoning tool.

rag-prover

A Retrieval Augmented Generation (RAG) stack built atop mathlib4, a massive collection of formal statements and proofs in Lean.

lean-kg

An interactive dependency graph of mathlib4.

number theory

TBA