Lean 4 Proof Engineer - Mathematical Formalization

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 about formal logic and proof? We're looking for mathematicians and formal verification specialists to translate rigorous human-written proofs into machine-verifiable Lean 4 formalizations — working at the very frontier of what modern proof assistants can express and automate. This is a fully remote, flexible contract role built for mathematically mature problem-solvers who love precision, structural elegance, and the challenge of capturing complex arguments in forms that machines can verify. 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 proofs across domains — algebra, analysis, topology, logic, discrete math — identifying hidden assumptions, gaps, and formalizable sub-structures Construct formalizations that test and extend the limits of existing proof assistants, especially where automation breaks down Investigate failure points in automated provers and articulate why they occur — missing lemmas, complexity barriers, insufficient library coverage, and more Collaborate with AI researchers to design and refine strategies for improving formal verification pipelines Develop 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 results and compare machine-verifiable structures against standard textbook arguments Surface deeper patterns and generalizations that become visible 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 Possess a strong foundation in rigorous proof writing and mathematical reasoning across core areas such as algebra, analysis, topology, logic, or discrete math Have hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or comparable formal proof systems — Lean 4 strongly preferred Find genuine satisfaction in taking a dense, elegant mathematical argument and expressing it in a form a machine can verify Appreciate precision and structural beauty, and bring both to every formalization you write Can work independently, asynchronously, and to a high standard of quality 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 fails or requires substantial manual scaffolding Prior experience with data annotation, data quality evaluation, or AI training workflows Strong communication skills for documenting formalization decisions, edge cases, and reasoning strategies Why Join Us Work on genuinely frontier problems in formal verification and AI research Collaborate with teams building and training cutting-edge AI models at leading research labs Fully remote and flexible — work on your schedule, wherever you are in the world Freelance autonomy with meaningful, intellectually stimulating task-based work Exposure to how advanced LLMs are trained to reason about mathematics Potential for contract extension as new projects launch