Job Opportunity
We are seeking mathematicians with deep training in rigorous proof construction and hands-on experience with formal proof languages.
* The selected candidate will be responsible for translating informal mathematical proofs into Lean (and related proof systems) with an emphasis on clarity, structure, and correctness.
* They will analyze generic and domain-specific proofs, identifying gaps, hidden assumptions, and formalizable sub-structures to ensure high-quality outputs.