Researcher - Lean 4 & Formal Proof Systems
Sheffield, TX
Contract
Remote
1 month ago
About the role
Researcher – Lean 4 & Formal Proof Systems (AI Training)
About The Role
What if your deep mathematical training could directly shape how AI understands and reasons about formal proof? We're looking for mathematicians and formal verification researchers to translate sophisticated mathematical arguments into machine-verifiable Lean 4 proofs — working at the very frontier of what automated reasoning can express and automate.
This is a fully remote, flexible contract role designed for researchers who love rigour, structural elegance, and the challenge of pushing proof assistants to their limits.
What You'll Do
Who You Are
Nice to Have
Why Join Us
About The Role
What if your deep mathematical training could directly shape how AI understands and reasons about formal proof? We're looking for mathematicians and formal verification researchers to translate sophisticated mathematical arguments into machine-verifiable Lean 4 proofs — working at the very frontier of what automated reasoning can express and automate.
This is a fully remote, flexible contract role designed for researchers who love rigour, structural elegance, and the challenge of pushing proof assistants to their limits.
- Organization: Alignerr
- Type: Hourly Contract
- Location: Remote
- Commitment: 10–40 hours/week
What You'll Do
- Translate informal, human-written mathematical proofs into precise, machine-verifiable Lean 4 formalizations
- Analyse proofs across domains — algebra, analysis, topology, logic, discrete mathematics — identifying hidden assumptions, gaps, and formalizable sub-structures
- Construct formalizations that test and expose the limits of existing proof assistants, especially where automation breaks down
- Develop clean, readable, and reproducible proof scripts aligned with mathematical best practices and Lean idioms
- Collaborate with AI researchers to design, refine, and evaluate formal verification pipelines
- Provide expert guidance on proof decomposition, lemma selection, and structuring strategies for formal models
- Investigate failure modes of automated provers — articulating why they struggle (complexity, missing lemmas, library gaps) and how to work around them
- Create Lean proofs that surface deeper patterns and generalizations implicit in the original mathematics
Who You Are
- Hold a Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a closely related field
- Have a strong foundation in rigorous proof writing across core mathematical areas
- Have hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or a comparable system — Lean 4 strongly preferred
- Deeply enthusiastic about formal verification, proof assistants, and the future of mechanized mathematics
- Able to translate dense, informal arguments into clean, structured formal proofs with precision and clarity
- Find genuine satisfaction in resolving gaps that automated tools cannot yet bridge
Nice to Have
- Familiarity with type theory, the Curry-Howard correspondence, and proof automation tools
- Experience with large-scale formalization projects such as Mathlib
- Exposure to theorem provers where automated reasoning frequently requires manual scaffolding
- Prior experience with data annotation, evaluation systems, or AI training workflows
- Strong communication skills for explaining formalization decisions, edge cases, and proof strategies
Why Join Us
- Work on cutting-edge AI research projects alongside leading labs and research teams
- Fully remote and flexible — work when and where it suits you
- Freelance autonomy with the structure of meaningful, intellectually stimulating work
- Contribute directly to advancing the capabilities of AI in formal reasoning and mathematics
- Potential for ongoing work and contract extension as new projects launch
Skills
Technology, Information and Internet