At a Glance
- Tasks: Translate complex mathematical proofs into structured Lean 4 formalizations and collaborate with AI researchers.
- Company: Join Alignerr, a leader in cutting-edge AI research and formal verification.
- Benefits: Fully remote, flexible hours, and the chance to work on groundbreaking AI projects.
- Other info: Freelance autonomy with opportunities for ongoing work and career growth.
- Why this job: Shape the future of AI by formalizing proofs and pushing the limits of automated reasoning.
- Qualifications: Master's degree in Mathematics or related field; experience with proof assistants like Lean.
The predicted salary is between 10 - 40 $ per hour.
About The Role
What if your deep mathematical training could directly shape how AI reasons about the hardest problems in formal verification?
We're looking for mathematicians and formal methods specialists to formalize advanced proofs in Lean 4 — working at the exact boundary where human mathematical intuition meets machine-verifiable logic.
About The Role
What if your deep mathematical training could directly shape how AI reasons about the hardest problems in formal verification?
We're looking for mathematicians and formal methods specialists to formalize advanced proofs in Lean 4 — working at the exact boundary where human mathematical intuition meets machine-verifiable logic.
This is a fully remote, flexible contract role.
If you've spent time wrestling with proof assistants, hunting for hidden assumptions in dense arguments, or pushing the limits of what automated reasoners can 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 clean, structured Lean 4 formalizations with an emphasis on correctness and reproducibility
- Analyze proofs across mathematical domains — identifying gaps, hidden assumptions, and formalizable sub-structures
- Construct formalizations that probe and expose the limits of existing proof assistants, especially where automation fails
- Collaborate with AI researchers to design and refine strategies for improving formal verification pipelines
- Develop highly readable, reproducible proof scripts aligned with mathematical best practices and Lean idioms
- Provide expert guidance on proof decomposition, lemma selection, and structuring techniques for formal models
- Formalize classical proofs and compare machine-verifiable structures against textbook arguments
- Investigate where automated provers break down — and articulate precisely why
Who You Are
- Hold a 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
- Genuinely excited about formal verification, proof assistants and the long-term future of mechanized mathematics
- Skilled at translating informal mathematical arguments into precise, structured formal proofs
- Mathematically mature — you find 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 contributing to large-scale formalization projects such as Mathlib
- Exposure to theorem provers in settings where automated reasoning frequently requires manual scaffolding
- Prior experience with data annotation, data quality, or evaluation systems
- Strong communication skills for explaining formalization decisions, edge cases, and reasoning strategies
- Why Join Us
- Work directly on cutting-edge AI projects alongside leading research labs
- Fully remote and flexible — work when and where it suits you
- Freelance autonomy with the structure of meaningful, technically demanding work
- Gain direct exposure to how advanced LLMs are trained on formal mathematical reasoning
- Contribute to work that is genuinely expanding the frontier of what AI can understand and verify
- Potential for ongoing work and contract extension as new projects launch
Applied Formal Methods Researcher (Lean 4) employer: Alignerr
As a leading AI research partner, we pride ourselves on fostering a collaborative and innovative work culture that empowers our employees to make a real difference in public health. With flexible hours and competitive pay, our Remote Health Policy & AI Content Specialist role offers unique opportunities for professional growth while contributing to meaningful projects that advance health equity. Join us to be part of a dynamic team dedicated to shaping the future of health information through cutting-edge AI technology.
