desargues

Desargues produces math training data for frontier reasoning models. Two axes:

• Informal mathematics — novel problems and proofs beyond IMO shortlist, nothing of it in any pretraining corpus.
• Formal mathematics — faithful Lean 4 formalizations of that work, expert-verified against the informal statement.

We work both axes end-to-end and deliver to frontier labs as SFT corpora, evals, and RL environments.

We are IMO medalists, and we've built the network of expert mathematicians labs can't source anywhere else.