Formal Verification Scientist

What You'll Do

• Translate informal mathematical proofs into clean, structured Lean 4 formalizations with an emphasis on clarity, correctness, and reproducibility
• Analyze both generic and domain-specific proofs to identify gaps, hidden assumptions, and formalizable sub-structures
• Construct formalizations that test the limits of existing proof assistants — especially in areas where automated tools struggle or fail
• Collaborate with AI researchers to design, refine, and evaluate strategies for improving formal verification pipelines
• Decompose complex arguments into well-structured lemmas and proof scripts aligned with mathematical best practices
• Investigate where automated provers break down and articulate the underlying reasons — missing libraries, complexity barriers, insufficient scaffolding
• Create Lean proofs that reveal deeper patterns or generalizations implicit in the original mathematics

Who You Are

• Holds a Master's degree or higher in Mathematics, Logic, Theoretical Computer Science, or a closely related field
• Has a strong foundation in rigorous proof writing across areas such as algebra, analysis, topology, logic, or discrete mathematics
• Has hands-on experience with Lean (Lean 3 or Lean 4), Coq, Isabelle/HOL, Agda, or a comparable proof assistant — Lean strongly preferred
• Deeply enthusiastic about formal verification, proof assistants, and the future of mechanized mathematics
• Able to translate dense, informal arguments into precise, machine-verifiable form with structural clarity

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 reasoning strategies

Selecionamos as principais informações da posição. Para conferir o descritivo completo, clique em "acessar"