About Functorial
Functorial builds tools that make formal verification practical: proofs checked by Lean, written and reviewed in a loop between mathematicians, programmers, and a superintelligence, so proofs and programs stay in sync.
human mathematician-verified autoformalization
Autoformalization of mathematics papers (definitions, lemmas, theorems and proofs) into Lean, in a feedback loop between a human mathematician and a superintelligence.
- 1
Read
Parse the LaTeX source of a paper into its mathematical structure.
- 2
Formalize
Draft Lean statements and proofs for each definition and result.
- 3
Validate
A human mathematician confirms each statement means what the paper says.
L∃∀N cards
open →Flashcards for learning Lean 4, one keyword per card. Answers are checked by real Lean, running in your browser as WebAssembly, so nothing is self-graded. Your progress stays in your browser.