Thrilled to announce Mistral AI’s new formal math team following our $2B funding round. We’re looking for people at the crossroads of formal math (Lean, Rocq, etc…) and AI.
We offer:
- Work on creating the state-of-the-art prover, autoformalizer, and automatic proof agent all in one model
- World class team (with Simon Sorg, Albert Jiang, Maxime Darrin and myself, and support from Guillaume Lample)
- Everyone is empowered to take action
- Hundreds of GPUs per capita with Mistral’s cutting edge reinforcement learning pipeline (responsible for Magistral and Magistral 1.2)
- Open research with publications
- Industry-leading salary
- Offices in Paris, London, and Palo Alto
Experience in AI required.
To apply: Send your CV and best work on AI and/or formal math to both jason.rute@mistral.ai and aj@mistral.ai, with <formal> in the email title.