The score soon became forgotten until its rediscovery in 1974 by Olivier Alain, who noticed an extra set of composition in one of the sources of the Goldberg Variations. After careful examination of the calligraphy, it became sure it was indeed a work by J.S.Bach. The score got its Bach - Werke - Verzeichnis catalogue number of "BWV 1087" and was premiered in december of that same year.
This guess Kepler assumed to be true became known as the "Kepler Conjecture" and it turned out to be a quite hard claim to mathematically prove. Noone could find a better packing than Kepler, but at the same time noone could prove that Kepler's was the "tightest" configuration of spheres possible.
That meant that potentially we weren't looking well enough. Maybe a better solution was possible but just harder to see?
In 1900, mathematician David Hilbert published a list of what he considered some of the great unsolved problems in mathematics up to that day. It consists of 23 problems.
Prooving the Kepler Conjecture true was one of them, still.
From Wikipedia, the free Encyclopedia
Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds.[1] This is a method of direct proof. A proof by exhaustion typically contains two stages:
- A proof that the set of cases is exhaustive; i.e., that each instance of the statement to be proved matches the conditions of (at least) one of the cases.
- A proof of each of the cases.
During 2023, I spent some time working on a code that could automatically check for canon solution in I-Counterpoint Species.
In short, I used Wrong Parallel Motions, Dissonances and Consonances as a filter to eliminate the unwanted ("wrong") canons, so that the computer would only output 100% "correct" results.
Since both notes and lenghts are finite, the possible combinations of notes within a fixed amount of time is, despite big, finite.
I had the curiosity to input the same 8 bass notes of BWV1087. Trying canons one by one would require a lot of time, but I was positive my little script could check all configurations in a matter of seconds.
In the 90s, mathematician Thomas Hales started working on a formal proof of the Kepler Conjecture with the help of computers and after the work done by László Fejes Tóth.
First, it was prooven that the seamingly endless number of sphere-configurations could actually be reduced to a finite list of over 5000 categories of configurations.
This meant that potentially, by checking all of the cases one by one and calculating their "density score", the problem could be solved by exhaustion. If at least one configuration was denser that Kepler's, the Conjecture was proven false.
Many hours would be required to make that many calculations. But luckily there are computers that can speed up the process by making the calculations for us
Nowdays, Hales proof is widely considered true, although its so long and complex that it was -and still is- very hard to verify. On top of that, it makes extensive use of computers to speed up the process of systematically validating mathematical statements.
My knowledge in mathematic is not sufficient to understand it.
But if I don't understand it, should I trust his proof and what he says?
From Wikipedia, the Free Encyclopedia
Philosophical objections to Computer-assisted proofs
Computer-assisted proofs are the subject of some controversy in the mathematical world, with Thomas Tymoczko first to articulate objections. Those who adhere to Tymoczko's arguments believe that lengthy computer-assisted proofs are not, in some sense, 'real' mathematical proofs because they involve so many logical steps that they are not practically verifiable by human beings, and that mathematicians are effectively being asked to replace logical deduction from assumed axioms with trust in an empirical computational process, which is potentially affected by errors in the computer program, as well as defects in the runtime environment and hardware.
