mathematics These are my projects related to mathematics. conductor A natural-language interface to the L-functions and Modular Forms Database (LMFDB). 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.