About the Role
What if your deep mathematical training could directly shape the future of AI reasoning? We're looking for mathematicians with hands-on experience in formal proof systems — especially Lean — to translate complex human-written arguments into precise, machine-verifiable formalizations at the cutting edge of AI research.
This is a fully remote, flexible contract role. You'll work on proofs that lie beyond the current reach of automated tools, helping map the frontier of what formal verification can express, capture, and automate.
- Organization: Alignerr
- Type: Hourly Contract
- Location: Remote
- Commitment: Flexible
What You'll Do
- Translate informal mathematical proofs into Lean (and related proof systems) with a focus on clarity, structure, and correctness
- Analyze domain-specific proofs, identifying gaps, hidden assumptions, and formalizable sub-structures
- Construct formalizations that test the limits of existing proof assistants — especially where tools struggle or fail
- Collaborate with researchers to design, refine, and evaluate strategies for improving formal verification pipelines
- Develop readable, reproducible proof scripts aligned with mathematical best practices and proof assistant idioms
- Provide guidance on proof decomposition, lemma selection, and structuring techniques for formal models
Who You Are
Must-Have:
- Master's degree (or higher) in Mathematics, Logic, Theoretical Computer Science, or a closely related field
- Strong foundation in rigorous proof writing across areas such as algebra, analysis, topology, logic, or discrete math
- Hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or comparable systems — Lean strongly preferred
- Genuine enthusiasm for formal verification, proof assistants, and mechanized mathematics
- Ability to translate informal arguments into clean, structured formal proofs
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 fails or requires manual scaffolding
- Strong communication skills for articulating formalization decisions, edge cases, and reasoning strategies
Ideal Candidate
You're a mathematically mature problem-solver who finds satisfaction in taking a dense, elegant human argument and expressing it in a form a machine can verify. You appreciate precision, structural beauty, and the challenge of resolving gaps that automated tools cannot yet bridge. The frontier of formal mathematics is where you want to work.
Sample Work
- Formalize classical proofs and compare machine-verifiable structures against textbook arguments
- Investigate where automated provers break down and articulate precisely why — complexity, missing lemmas, insufficient libraries
- Create Lean proofs that reveal deeper patterns or generalizations implicit in the original mathematics
Why Join Us
- Work on cutting-edge AI research alongside leading AI labs and researchers
- 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 AI reliability, formal reasoning, and high-integrity dataset creation
- Potential for ongoing work and contract extension as new projects launch