Projects: Sum of Three Squares

Stream: ItaLean 2025

[Pietro Monticone]

This thread is dedicated to the Sum of Three Squares:

• Repository: https://github.com/pitmonticone/SumsThreeSquares
• Informal & Formal Manager: @Bhavik Mehta

[Bhavik Mehta]

Have we had any aristotle progress on this yet, or still waiting?

[Abel Doñate Muñoz]

I made a pull request, aristotle did roughly half of the proof

[Pietro Monticone]

@Boris Alexeev opened an Aristotle-driven PR yesterday, but it doesn't exactly follow the original paper mentioned in the repository.

I think we might keep both of them. What do you think @Bhavik Mehta?

I'll experiment a bit later today anyway.

[Bhavik Mehta]

The reason I wanted to follow the original paper is that I think that's the right proof for mathlib. And in contrast, I think the ternary quadratic forms approach is neat and mathlib should have that theory but it's not clear that it's the right mathlib way to this result

[Pietro Monticone]

I see.