Researcher — Lean 4 & Formal Proof Systems (AI Training)
About The Role
What if your deep mathematical training could directly shape how AI reasons about formal proofs — pushing the boundaries of what machines can verify, understand, and learn
We're looking for mathematicians and formal verification specialists to translate sophisticated mathematical arguments into Lean 4, working on problems that sit beyond the current reach of automated provers. This isn't routine annotation work — it's frontier research at the intersection of mathematics and computer science, contributing directly to the development of cutting-edge AI systems.
This is a fully remote, flexible contract role. If you find beauty in rigorous proof structure and satisfaction in making a machine understand what only a human mathematician could express, this role was built for you.
- Organization: Alignerr
- Type: Hourly Contract
- Location: Remote
- Commitment: 10–40 hours/week
What You'll Do
- Translate informal mathematical proofs into precise, machine-verifiable Lean 4 formalizations with an emphasis on clarity, correctness, and structure
- Analyze proofs across domains — identifying hidden assumptions, logical gaps, and formalizable sub-structures
- Construct formalizations that stress-test the limits of existing proof assistants, especially where automated tools struggle or fail entirely
- Investigate and articulate why automated provers break down — whether due to complexity, missing lemmas, or insufficient library coverage
- Develop readable, reproducible proof scripts aligned with mathematical best practices and proof assistant idioms
- Collaborate with AI researchers to refine strategies for improving formal verification pipelines
- Provide expert guidance on proof decomposition, lemma selection, and structuring techniques for formal models
- Formalize classical proofs and compare machine-verifiable structures against standard textbook arguments
- Surface deeper patterns or generalizations implicit in the original mathematics through the formalization process
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 areas such as algebra, analysis, topology, logic, or discrete mathematics
- Have hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or a comparable proof assistant — Lean 4 strongly preferred
- Are deeply enthusiastic about formal verification, proof assistants, and the future of mechanized mathematics
- Can translate dense, informal mathematical arguments into clean, structured formal proofs independently
- Are comfortable working at the frontier — where the tools don't always cooperate and creativity is required
Nice to Have
- Familiarity with type theory, the Curry-Howard correspondence, and proof automation tools
- Experience contributing to large-scale formalization projects such as Mathlib
- Exposure to theorem provers in scenarios where automated reasoning frequently fails or requires significant manual scaffolding
- Prior experience with data annotation, data quality evaluation, or AI training workflows
- Strong written communication skills for explaining formalization decisions, edge cases, and proof strategies to interdisciplinary collaborators
Why Join Us
- Work on genuinely hard, intellectually stimulating problems at the frontier of formal verification and AI research
- Collaborate with researchers working on some of the most advanced AI models being built today
- Gain unique exposure to how large language models are trained and evaluated on mathematical reasoning
- Fully remote and flexible — work on your own schedule from anywhere in the world
- Freelance autonomy: choose your hours, work independently, and engage with a global research community
- Potential for ongoing work and contract extension as new projects launch
