Computational sum_four_squares

Stream: Is there code for X?

[Trebor Huang]

Do we have algorithms that decompose a number into the sum of four squares?

The current proof of that theorem seems to use classical logic, but since everything in the proof involves a finite range of objects, I think the classical axioms can be gotton rid of, right?

[Thomas Browning]

It's a finite search, so it should be too hard to write a slow algorithm.

[Eric Wieser]

Removing the classical axioms won't make it "computational" in any meaningful way - you need to convert it into a def for that

[Kevin Buzzard]

What does the fact that a proof exists have to do with writing an algorithm to come up with these numbers? Aren't these two distinct questions?

[Eric Wieser]

Well, a proof that the thing you're trying to calculate exists is a nice thing to have before wasting time on an algorithm to calculate something that doesn't

[Kevin Buzzard]

Sure but you can get that proof from Wikipedia. Its formalisation doesn't help, it's an independent thing, is what I'm suggesting.

[Stuart Presnell]

Well, a constructive mathematician might expect a term of the type ∀ n : ℕ, ∃ a b c d : ℕ, a^2 + b^2 + c^2 + d^2 = n to be a function that takes an n : ℕ as input and returns a quadruple a b c d : ℕ and a proof that they satisfy the equation. So from that perspective a proof and an algorithm are just the same, and so you might guess that it's the use of classical reasoning that lets you say "I can prove that a b c d : ℕ exist without working out what they are".

[Eric Wieser]

But that's not what ∃ x, p x means in lean, you want { x // p x} for that

[Stuart Presnell]

Sure, but I suspect this distinction trips up newcomers a lot and may have been at play in this question

[Kevin Buzzard]

The constructive mathematicians have gone off to use Coq and Agda a long time ago

[Trebor Huang]

Generally proofs may not directly reveal a program. But given that here the search space is just the integers in [0, p-1]^4, we can easily write a program that enumerates them, and the non-computational proof can then be used to prove that the search always yields a value, I think?

[Eric Wieser]

I don't think it's worth mathlib having the algorithm unless we have a less naive algorithm!

[Eric Wieser]

Perhaps we should have a version of docs#nat.find for docs#enumerable types like 4-tuples of nat

[Eric Wieser]

Which would be the API for the dumb algorithm

[Yaël Dillies]

You can just use lex ℕ (lex ℕ (lex ℕ ℕ)).

[Eric Wieser]

How does that help without the enumerable version of find?

[Eric Wieser]

ℕ × ℕ × ℕ × ℕ already has an enumerable instance

[Yaël Dillies]

Ah, that assumed an enumerablt version of nat.find, which is pretty easy to bodge together anyway.

[Ruben Van de Velde]

Well yes, but the enumerating program will work regardless of the proof - you certainly don't need it to be constructive or even be formalized

[Eric Wieser]

My point is that if we had the tools to easily build such enumeration programs in a single line from an existential, then mathlib wouldn't need to provide the programs themselves

[Yaël Dillies]

Note that, unless we have bootstrapping problems, one possibility is to straight up generalize nat.find to take in an enumerable instance.

[Eric Wieser]

It's in core so that's a bad option

[Eric Wieser]

Better would be to just add encodable.find next to docs#encodable

[Eric Wieser]

But it might exist already

[Kevin Buzzard]

The non-naive algorithms I know involve factoring, so if we want a non-naive algorithm then probably we first want a non-naive factoring algorithm. Fortunately we have tons of theorems about number fields :D

[Eric Rodriguez]

gnfs in lean when? ;b

[Kevin Buzzard]

The serious answer is to wait until Lean 4. Of course nothing needs verifying in this algorithm; who cares if it's bug-free, if it factors, it factors.