Every job listed here is analyzed by our AI to identify worldwide hiring — not just “remote in the US.” Our classification is actively being improved, some results may be inaccurate.
Worldwide Remote
Jobs reviewed for worldwide hiring.
Real Hiring Data
Country flags show the countries where each company has team members
Updated Hourly
Fresh jobs synced from thousands of career pages
Mathematical Formalization Specialist (Lean / Formal Proof Systems) 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 to translate rigorous human arguments into machine-verifiable formalizations — working at the bleeding edge of what proof assistants can express, capture, and automate. This is a fully remote, flexible contract role built for mathematicians who are passionate about precision, formal verification, and the challenge of pushing modern proof assistants to their limits. Organization: Alignerr Type: Hourly Contract Location: Remote Commitment: Flexible What You'll Do Translate informal mathematical proofs into Lean (and related proof systems) with an emphasis on clarity, structure, and correctness Analyze generic and domain-specific proofs — identifying gaps, hidden assumptions, and formalizable sub-structures Construct formalizations that test the limits of existing proof assistants, especially where automated tools struggle or fail Collaborate with AI researchers to design, refine, and evaluate strategies for improving formal verification pipelines Develop clean, reproducible proof scripts aligned with mathematical best practices and proof assistant idioms Advise on proof decomposition, lemma selection, and structuring techniques for formal models 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 Have hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or comparable formal systems — Lean strongly preferred Genuinely passionate about formal verification, proof assistants, and the future of mechanized mathematics Able to translate dense informal arguments into clean, well-structured formal proofs Self-directed and reliable when working independently on technically demanding tasks 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 breaks down or requires manual scaffolding Strong communication skills for articulating formalization decisions, edge cases, and proof strategies Sample Work You Might Do Formalize classical proofs and compare machine-verifiable structures against standard textbook arguments Investigate where automated provers break down — and document exactly why (complexity, missing lemmas, library gaps, etc.) Create Lean proofs that surface deeper patterns or generalizations implicit in the original mathematics Help map the frontier of what current formal verification tools can and cannot yet handle Why Join Us Work on genuinely 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, intellectually rigorous work Contribute to a growing field where your expertise directly advances the reliability and reasoning capability of AI systems Potential for ongoing work and contract extension as new formalization projects launch