01FORMAL MATHEMATICS
LeanMFG
Mean field games in Lean 4. Mathematical models, theory, executable algorithms, and machine-checked verification.
Varifold
Varifold is an open learning community studying formal verification, interpretability, and mathematical foundations of AI safety. We develop and share notes, tools, and open-source projects to support learning and verifiable knowledge discovery.
Formal verification Interpretability AI safety
Projects
Learning & open-source projects02LEARNING PROJECT
Mathematics for AI Safety
Mathematical notes on model learning, AI research feedback, interpretability, and agency, with open research questions and complete source materials.
03VERIFIED ALGORITHMS
LeanSort
Formal verification of sorting algorithms in Lean 4, with correctness proofs, execution traces, and operation-count bounds.
04NEURAL NETWORK VERIFICATION
neural-spec
Neural network verification in Lean. A trained XOR classifier with regional margin proofs over exact reals and a binary32 arithmetic model.