Paid Opportunity: Math Textbook Formalization in Lean 4

Stream: job postings

[Khai]

Update: Applications are currently paused. Thank you for your interest!

Mercor is a talent marketplace connecting experts with leading AI labs to improve frontier AI models.
We're looking for experts to formalize graduate-level mathematical statements from textbooks into Lean 4 (statement formalization only, no proofs required).

Requirements:

• Lean 4 and Mathlib experience (or experience with Coq/Isabelle/Agda, skills transfer well)
• Graduate-level mathematics background (Master's/PhD preferred, or competitive math experience)
• Comfortable reading research level pure mathematics

Compensation: Contract work, paid hourly

Application:
Complete a short qualifying quiz (30-45 min, 8 MC + 1 coding task). Use your primary email so we can contact you after completion.
https://docs.google.com/forms/d/e/1FAIpQLSe08PCQWOgjE_3fdDMXmMwld4iE2giYgM_AU2EvX8S-5C1Liw/viewform?usp=dialog

Questions or feedback welcome. Please reply here or email khaiquayle@c-mercor.com