Applied Formal Methods Researcher

About The Role

What if your deep mathematical training could directly shape how AI reasons, proves, and understands the structures underlying all of mathematics? We're looking for Applied Formal Methods Researchers to formalize advanced mathematical proofs in Lean 4 — pushing the boundaries of what automated reasoning can express, verify, and learn from.

This is a fully remote, flexible contract role built for mathematicians who live at the intersection of rigorous proof construction and cutting-edge AI research. If you find satisfaction in translating a dense, elegant human argument into something a machine can verify step by step, this role was made for you.

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

What You'll Do

• Translate informal mathematical proofs into precise, machine-verifiable formalizations in Lean 4 (and related proof systems)
• Analyze proofs across domains — identifying hidden assumptions, logical gaps, and formalizable sub-structures
• Construct formalizations that probe and expose the limits of existing proof assistants, especially where automation breaks down
• Collaborate with AI researchers to design, refine, and evaluate strategies for improving formal verification pipelines
• Develop clean, readable, reproducible proof scripts that align with mathematical best practices and proof assistant idioms
• Provide expert guidance on proof decomposition, lemma selection, and structuring techniques for formal models
• Investigate precisely where and why automated provers fail — complexity, missing lemmas, library gaps — and document your findings clearly
• Create Lean proofs that surface deeper patterns or generalizations implicit in the original mathematics

Who You Are

• Graduate-level mathematician (Master's 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 mathematics
• Hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or comparable formal proof systems — Lean strongly preferred
• Deeply enthusiastic about formal verification, proof assistants, and the future of mechanized mathematics
• Able to translate informal arguments into clean, structured formal proofs with precision and clarity
• A methodical problem-solver who appreciates structural beauty and thrives working at the frontier

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 significant manual scaffolding
• Prior experience with data annotation, data quality evaluation, or AI training workflows
• Strong communication skills for explaining formalization decisions, edge cases, and proof strategies to a research audience

Why Join Us

• Work on cutting-edge AI projects alongside leading research labs and AI teams
• Fully remote and flexible — work when and where it suits you
• Freelance autonomy with the structure of meaningful, intellectually demanding work
• Contribute directly to research that is defining how AI understands and reasons about mathematics
• Potential for ongoing work and contract extension as new projects launch