Lean Engineer - Formal Mathematics

Help a leading AI lab teach its models to write real, machine-checked mathematics in Lean. 1. Overview A leading AI lab is looking for Lean engineers, formal mathematicians and proof engineers to help its AI models state and prove mathematics correctly. You'll write and review Lean 4 proofs, turn informal math into precise formal statements, and help the lab's researchers judge whether a model's proof is not just accepted by the checker but actually proves the right thing. If you enjoy writing …