projects

mathematics

TBA

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.

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.