Job Description
Teaching rigorous mathematical reasoning to an AI system is one of the hardest unsolved problems in the field. Chegg is seeking PhD-level mathematicians to take it on. As a Mathematics SME, you will translate complex informal proofs into machine-verifiable formal structures, design research-level evaluation problems, and expose exactly where and why AI formal reasoning breaks down. This is frontier work at the boundary of mathematics and AI — fully remote, asynchronous, and highly specialised.
Core Responsibilities
- Translate informal mathematical proofs into verified Lean 4 code, emphasising clarity of structure, logical completeness, and alignment with Mathlib conventions
- Analyse complex proofs to surface hidden assumptions, proof gaps, and sub-structures that can be formalised independently
- Construct formalisation challenges that push the limits of current proof assistants — particularly in areas where automated tools consistently fail
- Develop clean, reproducible proof scripts and document the design decisions behind lemma selection, decomposition strategy, and formalisation approach
- Investigate and clearly articulate the reasons behind AI and tool failure modes — whether caused by missing lemmas, complexity spikes, or library gaps
Key Qualifications
- Master’s degree or PhD in Mathematics, Mathematical Logic, Theoretical Computer Science, or a closely related discipline
- Strong command across core areas of pure mathematics — algebra, analysis, topology, combinatorics, or mathematical logic
- Hands-on experience with Lean 4 or a comparable interactive proof assistant such as Coq, Isabelle/HOL, or Agda
- Exceptional ability to write rigorous mathematics clearly and precisely in English — notation, derivation flow, and logical integrity all matter
- Self-directed; capable of sustained independent focus on demanding problems
Nice to Have
- Active contributions to Mathlib or other large-scale formalisation projects
- Background in formal methods applied to software verification or type theory
- Experience in econometrics, computational mathematics, or applied statistics
Why Chegg
- Fully remote and flexible
- Task-based commitment — typically 10–40 hours per week
- Among the most specialised and premium engagements in the programme
- Ongoing frontier AI mathematics research for outstanding contributors