Formal Verification Scientist (Lean 4 & Mathlib)

Formal Verification Scientist (Lean 4 & Mathlib)

About the Role

What if your deepest mathematical knowledge could directly shape how AI reasons about formal proof — permanently expanding the boundary of what machines can verify and understand?

We're looking for mathematicians with serious formal verification experience to translate advanced mathematical arguments into machine-verifiable Lean 4 proofs. This isn't routine formalization work. You'll be operating at the frontier — tackling proofs that push or exceed the current limits of automated proof assistants, and helping leading AI research teams understand exactly where those limits lie and why.

This is a fully remote, flexible contract role built for mathematicians who think precisely, work independently, and care deeply about the structure underlying rigorous argument.

• Organization: Alignerr
• Type: Hourly Contract
• Location: Remote
• Commitment: 10–40 hours/week

What You'll Do

• Translate informal mathematical proofs into clean, structured, machine-verifiable Lean 4 formalizations
• Analyze proofs across domains — algebra, analysis, topology, logic, discrete mathematics — identifying hidden assumptions, gaps, and formalizable sub-structures
• Construct formalizations that stress-test the limits of current proof assistants, and clearly articulate where and why they struggle
• Collaborate with AI researchers to design and refine formal verification pipelines and evaluation strategies
• Develop reproducible, well-structured proof scripts aligned with mathematical best practices and Lean idioms
• Provide expert guidance on proof decomposition, lemma selection, and structuring strategies for formal models
• Formalize classical results and compare machine-verifiable structures against textbook arguments to surface deeper patterns and generalizations

Who You Are

• Holder of a Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a closely related field
• Deeply trained in rigorous proof construction across core mathematical areas
• Experienced with Lean (Lean 3 or Lean 4), with Lean 4 strongly preferred — or with comparable systems such as Coq, Isabelle/HOL, or Agda
• Genuinely passionate about formal verification, proof assistants, and mechanized mathematics
• Able to take a dense, informal mathematical argument and render it in a form a machine can understand — without losing mathematical meaning
• Self-directed and comfortable working asynchronously at a high level of precision

Nice to Have

• Experience with large-scale formalization projects such as Mathlib
• Familiarity with type theory, the Curry-Howard correspondence, and proof automation tools
• Exposure to theorem provers in settings where automated reasoning frequently requires manual scaffolding
• Prior experience with data annotation, evaluation systems, or structured data quality workflows
• Strong ability to communicate formalization decisions, edge cases, and reasoning strategies clearly in writing

The Ideal Candidate

You're a mathematically mature problem-solver who finds genuine satisfaction in taking an elegant human argument and expressing it in a form that a machine can verify. You appreciate structural precision, notice the gaps that automated tools miss, and are energized — not frustrated — by the places where formal verification is still an open problem. You work well independently, document your reasoning carefully, and enjoy contributing to something at the actual edge of what's possible.

Why Join Us

• Work directly on cutting-edge AI research projects alongside world-leading research labs
• Fully remote and flexible — structure your hours around deep work, on your schedule
• Freelance autonomy with access to some of the most intellectually challenging mathematical problems in AI today
• Exposure to advanced LLMs and insight into how formal reasoning capabilities are built and evaluated
• Potential for ongoing work and contract extension as new projects launch