Sign Up for the Aristotle API!

Stream: Machine Learning for Theorem Proving

[(deleted)]

#announce > Sign Up for the Aristotle API!

I knew this day would come. GPT-5 is already quite good.

[(deleted)]

Has anyone tried the API?

[Alex Meiburg]

If you're curious to see the kind of 'raw' outputs I've gotten from the API: 1, 2 -- those got cleaned up and merged to Mathlib -- and 3, 4 that I would like to eventually clean up and PR.

[(deleted)]

How long does it take to run

[(deleted)]

I care a lot about speed

[(deleted)]

Because GPT-5 can already do a lot it's just slow

[Lenny Taelman]

Vikram Shanker said:

[...] The API is designed to complete the sorries in your project - here are few more details: [...]

Great timing, we are having the SorryDB Hackathon in Amsterdam right now! We would be excited to test Aristotle against >3000 real-world sorries!

[Chris Hughes]

It proved the formula for the volume of a simplex with vertices at the origin and each of the basis vectors of R^n. I was impressed by that; I tried myself and didn't manage.

[Eric Wieser]

Volume in the measure theoretic sense?

[Jared green]

will we get periodic updates on benchmark performance?

[Yury G. Kudryashov]

See also #mathlib4 > Discussion thread for Aristotle API for a thread targeted at users who don't care about AI systems development.

[Eric Rodriguez]

just want to note that we also released our tech report on https://arxiv.org/abs/2510.01346 :)

[Kevin Buzzard]

Eric Rodriguez said:

just want to note that we also released our tech report on https://arxiv.org/abs/2510.01346 :)

Reference 42 you have "freiman ruzsa" presumably because of TeX's arcane biblio system. Try {F}reiman--{R}uzsa in the bibtex?

[Kevin Buzzard]

PS congratulations on becoming the first tech company to actually write a paper about a computer trying an IMO competition, rather than just a blog post! [edit: I'm wrong, apparently this honour goes to Seed-Prover]

[Yury G. Kudryashov]

AFAIK, there are tech reports from other companies too. They just forgot to announce it here.

[Jason Rute]

@Kevin Buzzard here is the tech report of Seed Prover which got a silver (or gold if given more time) in the IMO. https://arxiv.org/abs/2507.23726. I thought @Thomas Zhu shared it here on Zulip, but maybe I’m mistaken.

[Thomas Zhu]

The Seed-Prover paper was shared to #announce here: https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Seed.20Prover.20Achieves.20Silver-Level.20Score.20at.20IMO.202025/near/532198800.

[Eric Wieser]

Eric Wieser said:

Volume in the measure theoretic sense?

Could you share the statement, Chris?

[Chris Hughes]

theorem problem {n : ℕ} :
    MeasureTheory.volume.real (convexHull ℝ ({(0 : Fin n → ℝ)} ∪
      Set.range (fun i : Fin n => Pi.single i 1))) =
      1 / n.factorial

[Dhyan Aranha]

It looks like Dan Halpern-Leistner's name is misspelled in the arxiv paper announcement.