Lean 4 Proof Engineer — Mathematical Formalization

About The Role

What if your deep mathematical training could directly shape how the world's most advanced AI systems reason, prove, and think? We're looking for Lean 4 Proof Engineers to translate rigorous mathematical arguments into machine-verifiable formalizations — working at the very frontier of what proof assistants can express and automate.

This is a fully remote, flexible contract role built for mathematicians who find beauty in precision and satisfaction in resolving the gaps that automated tools cannot yet bridge.

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 clarity, correctness, and reproducibility Analyze domain-specific and general proofs to identify hidden assumptions, gaps, and formalizable sub-structures Construct formalizations that test the limits of existing proof assistants — especially where automated tools struggle or fail entirely Collaborate with AI researchers to design, refine, and evaluate strategies for advancing formal verification pipelines Investigate breakdown points in automated provers and articulate why they occur — missing lemmas, complexity barriers, insufficient libraries Develop highly readable proof scripts aligned with mathematical best practices and proof assistant idioms Provide expert guidance on proof decomposition, lemma selection, and structuring techniques for formal models Formalize classical proofs and compare machine-verifiable structures against their textbook counterparts

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 Possess hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or comparable proof systems — Lean 4 strongly preferred Are deeply enthusiastic about formal verification, proof assistants, and the future of mechanized mathematics Can take a dense, informal argument and express it precisely in a form a machine can verify

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 where automated reasoning frequently fails or requires extensive manual scaffolding Prior experience with data annotation, evaluation systems, or AI training workflows Strong communication skills for articulating formalization decisions, edge cases, and reasoning strategies to non-specialist collaborators

Why Join Us

Work on genuinely frontier problems alongside world-leading AI research teams and labs Fully remote and flexible — structure your work around your life, not the other way around Freelance autonomy with the substance of meaningful, intellectually demanding work Gain direct exposure to how cutting-edge large language models are trained and evaluated Contribute to mapping the boundary of what formal verification can express and automate Potential for ongoing work and contract extension as new projects launch