Talk:List of long mathematical proofs
 | This article is rated List-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||
| |||||||||||
The 200 TB for the Boolean Pythagorean triples problem is not "data", but a "proof"
[edit]The statement
"2016 Solving boolean Pythagorean triples problem required generation of 200 terabytes of data."
is not correct: the 200 TB is not data, and is was also not "required" to solve the problem. These 200 TB are the formal proof of the underlying propositional tautology, *extracted* (and compressed) from the run of the SAT solver
So this is a proper mathematical proof, rather different from the other entries currently under "Long computer calculations" except of the penultimate entry on the Erdős discrepancy conjecture (which is of a similar nature). The SAT solver said "unsatisfiable" (which corresponds to saying that the underlying propositional formula is indeed a tautology). But the 200 TB then actually give a formal proof.
For the other non-SAT entries, one has to trust the calculation (software and hardware), while for the two SAT entries, a formal proof has been extracted, which is precisely specified (and also rather simple in nature), which can be verified completely independent of the original calculation.
So I believe a third section is needed, for large (verified) proofs coming from ATP (automated theorem proving); in a sense this is similar to the section "Long proofs", in that actually mathematical statements are proven (without some reference to some numerical data), but it is different in that these proofs have been found by ATP (i.e., by computers).
A link to https://wiki.riteme.site/wiki/Automated_theorem_proving might be useful here. Oliver Kullmann (talk) 17:04, 5 June 2016 (UTC)
Another quite misleading statement is "and the length is due to long but routine calculations.": There is absolutely no guarantee that the SAT solvers terminate within the life time of the universe (or far beyond), but the exponential explosion has to be beaten with novel techniques (which have been developed in SAT solving over the last 60 years).
This is similar to ATP in that also there a vast search space has to be explored. It is definitely not the case, that some algorithm designer parcels out the task, and then it is just a question of having enough resources to carry out the task.
Again, this is an argument for having a third section, perhaps called "Proofs found by ATP methods". — Preceding unsigned comment added by Oliver Kullmann (talk • contribs) 17:27, 5 June 2016 (UTC)