The longest mathematical proof ever

[@DrTrefor]

Clarifications: 1) In the definition of Schur number, we are talking about the largest integer such that *there exists* a coloring with no monochromatic solutions to a+b=c. You can always do a stupid colorings like all one color, the question is how high can we get where we can find at least one possible coloring without any monochromatic triples. 2) A few of you noticed the distinction between demanding each number has AT LEAST one color and demanding each number has AT MOST one color (put together, each number gets exactly one color). In the video I only implemented the former. Partly, this was because the expressions were long and I wanted it brief for the video, but partly this is because when using SAT solvers, a technique called blocked clause elimination ends up eliminating the extra causes for the AT MOST direction. Some of the comment suggestions was just to use XOR instead of OR, but SAT solvers apply to things in something called "conjunctive normal form" which is just long series of and statements of or statements, so when encoding we break up the XOR statements into multiple OR statements. Check out the section on the paper on symmetry breaking for further reading here. 3) Just for fun. What the "longest" mathematical proof is depends a bit on interpretation. Another contender (and won the guiness record) is the classification of finite simple groups, involving hundreds of papers combined.

[@Player_is_I]

Epic video! ❤

[@deoxal7947]

So are you saying the proof is to find a coloring pattern that doesn't have any monochromatic triples for all integers? I was really confused how you picked the ordering at the beginning of the video.

[@FrankHarwald]

Content quality: SUPER! Production quality: meh. Man, your recording is kind of bad, you new better/new recording equipment/staff.

[@DjVortex-w]

Quite many years ago, when commenting on another proof that similarly had a huge amount of computer-generated data attached to it, a mathematician said that (paraphrasing) "a good mathematical proof is like a poem. This proof is like a phonebook." He didn't like that proof much.

[@DrTrefor]

That’s an awesome line lol

[@JMUDoc]

It was said about the proof of the Four Colour Theorem, but there's no definitive source for the quote.

[@steffenbendel6031]

There probably is s theorem that not all problems that have solutions have a nice short proof.

[@michaelleue7594]

@@steffenbendel6031 That would be a conjecture, not a theorem.

[@stevenfallinge7149]

@@steffenbendel6031 One classic example of such a "messy" proof is the proof that that a random walk along a grid (almost) always returns to itself in 2D but not in 3D. It's just a bunch of computation that a series converges or diverges, it's very much "go in an do it" rather than anything "elegant."

[@razvanrusan9319]

This is why mathematics- in a very general and abstract sense- scares me. What if some answers *could* be known, but they're simply too complicated for our minds to understand?

[@fungouslobster5123]

this happens a lot so we have to develop new tools to make them more interpretable but there probably is stuff that can never be fully understood

[@MinecraftMasterNo1]

Mathematics is fundamentally incomplete or inconsistent anyway. And we cannot demonstrate its consistency. There is already a fundamental leap of faith when we do math and choose to believe our results to be correct.

[@2299momo]

@@MinecraftMasterNo1 That's different than what OP is considering

[@ckq]

I mean we know a lot of stuff. The stuff we don't know are left for conjectures and the future

[@MinecraftMasterNo1]

@@2299momo If we cannot prove even results we know to be true or even be sure that things we believe to be "true" are actually true or if our formal system is inconsistent, what would even more complex results change? absolutely nothing

[@deleted-something]

God may forgive the peer reviewers 🤣

[@DrTrefor]

lol right:D

[@crazyape968]

16:29 You say 2 terabytes here but 2000 terabytes at the beginning of the video. I assume the 2000 is correct since a "mere" 2TB is nothing these days.

[@DrTrefor]

Oh yes, I meant 2 PETAbytes

[@QuardGame]

Props to the guy in 90s who found solution with 160 numbers

[@DigitalJedi]

Those poor, poor pentiums.

[@iMíccoli]

True, what a legend.

[@stefangrosser6466]

Another interesting question on could ask is, "Can we give a much much shorter proof that S(5) = 160?". As you say in your video, the runtime and computational history of a SAT solver is quite literally a proof of the theorem it is showing. If you pick any SAT solver, its rules define some small subset of first order logic. For the SAT solver in this paper, let's call this fragment of logic T. We can very generally ask, is there a shorter T-proof at all which demonstrates that S(5)=160? This is the field of Propositional Proof Complexity (which is my field :) ), where you try to show that powerful systems of deductions can require very long (even exponential size) proofs to show that a theorem is true. The simplification rules you show in the video are part of the Resolution propositional proof system, one of the most foundational and well studied proof systems. In general, SAT solvers use much more powerful deductions, and define proof systems of which it is open to get exponential lower bounds for proof sizes. I do not know exactly what proof system T the SAT solver in this paper corresponds to, but trying to show that no shorter proof is possible is fascinating and most likely wide open.

[@DrTrefor]

Ya that's a really interesting questions for sure, thanks for sharing:)

[@scudlee]

Presumably you could simplify the statements slightly by fixing the colors of 1 and 2, since you know they must be different, and any successful coloring would be also be true with the colors permuted however you like.

[@DrTrefor]

Ya actually I didn’t put it in the video but the author does a lot of work with this idea and “symmetry breaking”more generally

[@JohnDoe-ti2np]

@@DrTrefor It's just one author, right? Marijn Heule?

[@almscurium]

@@JohnDoe-ti2npclearly not

[@JohnDoe-ti2np]

@@almscurium Who are the other authors?

[@Faroshkas]

​@@JohnDoe-ti2npJames Hegensson

[@yfidalv]

the animations at 11:52 with the logical clauses cancelling out was so satisfying, that was a great segment

[@andrewharrison8436]

There are just these "easy" proofs that depend on doing something in principle but doing that thing in practice is really hard. The proof of an infinite number of primes is an obvious example, producing a few thousand primes is easy enough but factorising their product + 1 is a really hard problem but in principle it generates a prime we haven't listed yet. Ramsey theory seems to be a rich source of these kinds of proof, if it's big enough there will be something but how big is left as an exercise for the reader!.

[@DrTrefor]

Ya Ramsey theory has all these theorems about how eventually some structure is guaranteed to occur eventually and some of the proofs are quite nice and elegant, but the computations sure get super long!

[@sstadnicki]

That's _a_ proof for the infinitude of primes, but it's worth noting that there are a lot of them out there and many of them don't require any calculation to prove. My personal favorite goes through information theory, though it assumes unique factorization: we show that for any representation of numbers as a string of bits, for all n there's at least one number of at most n bits whose representation is at least n bits long. This is just a counting argument: there are 2^n such numbers but only 2^n-1 bit strings of length

[@unvergebeneid]

It's kind of impressive that in the 90s, they found a lower bound that turned out to be the actual solution.

[@DrTrefor]

Ya for sure. There are some shortcuts to help search (notice that the one for 3 is a palindrome? So is the example for 5).

[@katakana1]

@@DrTrefor Could that be true for any odd number? (including the trivial case of 1)

[@KanaalJo]

it is also easier in the sense that you have to find only 1 coloring that satisfies the constraints (there are probably many 5-colorings for the first 160 integers). That actually makes me wonder now if you could predict more or less where the change in satisfiability and unsatisfiability occurs by counting the amount of satisfiable solutions as the number of integers grow.

[@codahighland]

Woo! Shout out to ACL2, I haven't heard about that since I was working on my honors thesis 20 years ago. Good stuff!

[@rosiefay7283]

3:08 I think you mean "such that *it is possible* to colour 1..n with k colours so that there are no monochromatic solutions to a+b=c".

[@DrTrefor]

Exactly, thank you! Certainly many colourings (like all just one colour) will have monochromatic triples.

[@CrateSauce]

British detected. Activating Project Webster... *color

[@jesusthroughmary]

Your "correction" is merely stylistic, it's the same in substance as what was in the video

[@DrTrefor]

@@CrateSauceCanadian in this case!!

[@leif1075]

​@DrTrefor Off topic Trefor can you PLEASE PLEASE SHARE HOW you don't get fed up and bored and tired doing math?? And how can I be a genius like Einstein or Ramanujan? Hope to hear from you PLEASE

[@RhettRobinson]

Very cool! Given a computational proof like this, are we able to get interesting insights from the proof? The advances on algorithms is great to see though!

[@DrTrefor]

I don’t think it yields some interesting insight, although in other cases it can such as the computer finding a conjecture we didn’t think about before

[@purplenanite]

if you encoded the colors as binary digits, you could likely decrease the number of variables a bit, while also de facto encoding that each color can only occur once. like - if there were four colors, then 2 variables would be needed : TT -> color 1 TF -> color 2 FT -> color 3 FF -> color 4 for 5 colors though, you would need 3 bits, so the savings aren't as great. Although i don't know if it parallelizes more efficiently.

[@GeoffryGifari]

Questions on mathematical proofs, but not really linked to the problem in the video: 1. One mathematical statement can have multiple ways to prove it right? If each proof has a different length, is there a way to determine the proof (step-by-step) with minimal length? 2. Generalizing the first question: since math deals with abstraction, can the proofs themselves be treated as mathematical objects with certain properties?

[@lietpi]

Certainly you can treat proofs as objects of some sort. For instance, in the theory of "propositions-as-types", a proof is a term of a particular type that represents the proposition. Depending on how this term is represented, you can even have a notion of length. I believe determining the minimal proof length is an undecidable problem, since we can search all proofs of that length for a proof of our statement in finite time. But we already know that the problem of proving statements is undecidable in general.

[@creativenametxt2960]

determining minimal proof size should be possible if we know that the proof exists (iterate over all possible proofs, starting with the ones with minimal length up until you find one) the problem is that such a method is unviable, it's gonna take too much time to compute there presumably are better options than what I just described, but it doesn't seem likely that it's an easy task for the general case at least

[@columbus8myhw]

For the first question, nobody knows a good way to do this in general. (In theory you could "brute force" this but it would take much longer than the age of the universe to do.) For the second question: yes! This is known as "proof theory". Proofs depend on the axioms you have: the more axioms you have, the more theorems you can prove, but if you have too many axioms you might have accidentally introduced an inconsistency. Perhaps the most famous result of proof theory is Gödel's first incompleteness theorem, which (in a sense) shows that there is no "strongest" axiom system.

[@1.4142]

the audio sounds a bit compressed

[@DrTrefor]

I really hate audio - I THOUGHT I had my normal set up but something must have been set wrong unfortunately:/

[@jjjjulian]

@@DrTrefor you can use AI to enhance audio quality!

[@blockshift758]

Peak of PFP checks out

[@davethesid8960]

2:09 But you don't have two 1's, so that's cheating.

[@alexbenton226]

5:10 bruce force?

[@DrTrefor]

Um lol

[@TRex-fu7bt]

Really nice SAT explanation

[@perpetummobile5985]

Small historical comment: although it is of course correct to say that Schur's theorem belongs to the area of Ramsey theory, I feel like it is important to mention that Issai Schur proved his theorem at least 11 years before Ramsey proved his eponymous Ramsey theorem, and at the time Schur proved it Ramsey was likely a middle schooler still.

[@martinepstein9826]

I feel like 5 is usual the number where very fast-growing or difficult to compute sequences show their teeth. - The 5th busy beaver number was only recently confirmed to be 47,176,870 - 2^(2^(2^2) is a manageable number, 2^(2^(2^(2^2))) is not - The Ramsey number R(4,4) is known, the Ramsey number R(5,5) is not - The 4th Schur number isn't too difficult to find, but the 5th is at the very limit of our capabilities.

[@ocks_dev_vlogs]

5:16 while this number iis the max amount of combinations, a lot of these would be invalidated immediately, like take this example. If I use the colors A B and the numbers 1 2 3 4, coloring them 1A 2B 3B 4A is functionally the same as coloring them 1B 2A 3A 4B, which reduces the amount of combinations by a decent margin

[@icemelts3191]

i loved math got depressed then i hated everything, changed my major, now i just spend a lot of time reminiscing the good times... thus, this comment on a video of math proves..

[@tristanballman9262]

Can we establish better bounds by solving the problem for subsequences of the positive integers? Edit: or perhaps by analyzing the relationships between N, 2N, 3N... which are all isomorphic under addition and can be colored with the exact same patterns.

[@klausklausen4301]

I kinda expected the Classification of finite simple groups, but this was interesting nonetheless.

[@DrTrefor]

That definitely wins for longest written “by hand” by humans, actually i think it even won the Guinness book of world records for it!

[@eclipse1353]

@@DrTrefor I don´t quite recall that one, but there was a more than 300 page long proof that 1+1=2

[@cosmo1248]

​@@eclipse1353 Not quite, the majority of the first 300 pages are setting up the system, only some of which are needed to show that 1+1=succ(1)=2. I think the classification of finite simple groups is 2000 pages long

[@Utesfan100]

That is only 100,000 pages of journal articles. That can fit on most hard drives now adays.

[@purplenanite]

I think I found a pretty alright lower bound, in two interesting ways If you take a solution of n-1 colors: S(n-1), the first color we add after that (S(n-1)+1) must be our new color (say green) then the only thing preventing us from coloring everything green is that (S(n-1)+1)*2 cannot be green but we can color green from S(n-1)+1 ... 2S(n-1)+1. And then, we can repeat the original solution for S(n-1), as it's now far away enough for interference to go away (sorta) which gives us a coloring of n colors with length 3*S(n-1)+1. (it also preserves symmetry - if the solution to n-1 is symmetric, this will also be!) Alternatively, we can make our first color (say blue) on the numbers 3n+1, like 1,4,7,10... since (3n+1)+(3m+1)=3(n+m)+2, this coloring is fine. now we consider the gaps. the first gap is 2,3 - next is 5,6 - 8,9, etc but consider how these numbers add. 2+2=4 (which is blue, and is covered) 2+3=5 3+3=6 5,6 are in the next gap up. An in general, all the numbers in gap "n" + gap "m" either are blue (end up in 3n+1), or end up in gap "n+m". Therefore, if we make all the numbers in a gap share the same color, we can reduce it back to the original problem, but smaller and with one less color. If you make this coloring S(n-1), then this will also give you 3*S(n-1)+1, but in a different way.

[@tsuwako7497]

I'm certain Schur found that lower bound. It gives the inequality S(n) >= 3*S(n-1)+1. If you iterate S(n-1) >= 3*S(n-2)+1 and so on you get S(n) >= (3^n -1)/2. That said, this lower bound gives S(5) >= 133 and S(6)>= 481 while we know S(6)>=536... It seems that it gets less precise as we take a bigger n

[@evgiz0r]

Really cool, enjoyed it a lot. Sounds like the SAT solvers integrate such parallism methods into them ( or some higher level library ). I wonder if you could use the same method to find multiple 160 solutions, find some patterns in those to optimize searches for even larger scales ( better probably for succesful searches ) It is also common to add more rules to the problem, so it could fail faster. For example you can deduce that no following numbers will be blue after you color 1 with blue. But of course its a trade off. Will try on some of our high level solvers and see how bad those are 😅

[@DrTrefor]

Ya this method additionally categorized all of the (millions of) solutions in the 160 case, and many do have nice patterns like being palindromes

[@PitchWheel]

As a non matematitian i'm astonished by the fact that such a simple problem cannot be solved by understanding the underlying patterns and symmetries that certainly exist. For example, chosen a number c divide it by two, then a and b will every time equally distant from that result, giving the solution a certain predictability and order. It's very strange that brute force is the only possible way. This furthermore makes me wonder when you clearly created a very simple algorithm for the first easiest solution, an algorithm that apparently could lead in my eyes to some graph theory solution

[@sstadnicki]

One of the problems is that there's less symmetry and pattern here than you might think; note that there was a proof for two colors in the video, but for three there was just a configuration given, not a proof that it's maximal. When you try and actually walk through a proof for yourself you'll find that it's a sort of educated 'guess-and-check', a lot like solving a sudoku; you can cut off a lot of possible options / branches fairly short but you wind up exploring a few in great depth. This sort of structure (a search tree) is actually pretty well-known from the early days of computer chess and we have a pretty good understanding of what kind of speed-ups you can get with it; it generally takes the number of cases from roughly n^d to n^(d/2), roughly a square root. So here you'd be going from 5^160 to 5^80 - an immense reduction, but the reduced result is still well outside the reach of analysis.

[@sstadnicki]

A good illustration of the lack of structure is the construction of _Golomb Rulers_ ( en.wikipedia.org/wiki/Golomb_ruler ) : they've got a very similar flavor to these non-monochromatic colorings, but if you look at the examples there's little rhyme or reason to them and even looking at the optimal lengths, almost any conjecture you might want to make about these as a sequence starts to fall apart within the first couple dozen values.

[@ZoranRavic]

​@@sstadnicki "for three there was just a configuration given, not a proof that it's maximal". It's easy to check and see that 13 is max for 3 colors, but it wouldn't fit nicely in a video. Coincidentally there are 3 possible configurations and they are all almost identical. Only for 4 and more colors it gets chaotic.

[@phyarth8082]

Four color map theorem was first time then computation proved mathematical theorem.

[@adeldude13]

Amazing video as always

[@johnchessant3012]

pretty cool! also I did a double take at 14:31 haha

[@DrTrefor]

Haha 🤣

[@yanntal954]

So if i got this straight, the proof actually was that you cant color using only 5 colors the numbers from 1 to 161? If thats the case, then I can see why the verification should take just as long, because this would be a coNP-Complete problem, namely, deciding that a formula is not satisfiable?

[@DrTrefor]

Exactly. You can do it for 160, can't do it for 161

[@yanntal954]

@@DrTrefor My confusing was related to the fact that this looked like it's going to find a satisfying assignment, thus solving an NP problem and so the verification wouldn't have been as difficult as solving it in the first place. However, this as far as I understand now, was not the case. They solved a problem outside NP, thus having a proof as difficult to verify as it is to find! It was known for over 30 years that 1,...,160 was possible with 5 colors and they showed 1,...,161 was not.

[@farkarf]

2 PBs is huge. So is 13 years of compute (was it 13? can't remember). I wonder if cryptographic methods can play a useful role for the archival of verified machine generated proofs. Say a compact artifact that asserts the verifier successfully verified the output of the program -- a non-interactive zero knowledge proof, maybe. If in the future the math community is to generate such proofs at scale, it would be useful not to have to archive the proof itself but only program [that generates the proof] along with a cryptographic proof that its output was verified. Is the issue of the *archival* of computer generated proofs itself an area of research?

[@matthewlloyd3255]

20-25 years ago I studied Applied Mathematics - things like Fluid Dynamics, various numerical methods and other things very useful to Engineering and related disciplines. I'm glad I didn't study pure mathematics - I much prefer mathematical knowledge that has some fairly obvious direct application to real world stuff. Most of this number theory sort of thing just seems to be at the edge of being practical - at least a lot of the time, but not always. My attitude is not dissimilar to the kids I taught later, "Sir...when are we ever going to use this maths?"

[@benjaminshropshire2900]

With regards to the balance between breaking it up and "just work longer", I kinda wonder what the motivation for ever going with "just work longer" would be? I'm thinking it suggests something about the distribution of solution times that it's faster to do that then break up everything that doesn't solve quickly. On the other hand, you might be able to have you cake and eat it too if the SAT solver could take an intermediate state of a problem and on demand split it into halves that can be processed on concurrency. If a solver could be structured that way, then you just trigger that on the longest running shard any time you have unused compute. That said, I'm now wondering if that's what they did? (One interesting property of tree search algorithms is that they can be insanely sensitive to how you traverse things. Even very tiny improvements to the choice of how you proceed can make many order of magnitude changes in compute time. I first ran into this with alpha-beta pruning where just by changing the fixed order of traversal of sub trees I got a change in the "effective branching factor" from something like 3.07 to 3.01 for something like a 100x speedup.)

[@letsmakeit110]

I've used this before when writing sudoku solvers and rpg party optimizers, but I didn't know the concept already had a name. I just called it partial combinations.

[@user-pr6ed3ri2k]

15:47 I wonder how they formulated S(5) without knowing how many "a+b≠c if a,b,c are the same color" statements they should add

[@orenamir2]

Is there quantum algorithm for finding schurs number? Seems like there should be

[@SobTim-eu3xu]

Great video!)

[@DrTrefor]

Thanks!

[@chrisjohngrima9761]

Fermat if he had extra papers

[@mcol3]

So what is S(5)? 160?

[@DrTrefor]

Ha yes! I suppose I should have said that explicitly somewhere:D

[@MrConverse]

8:55, did you say “colored true” when you meant to say “colored blue”? Kinda a fun verbal misstatement. Great video!

[@DrTrefor]

Um lol that is quite the “speako”:D

[@kaishang6406]

the example encoding you give isn't correct. it should be "p1b xor p1y" instead of "p1b or p1y" where a xor b is "a or b and not (a and b)".

[@electricnezumi]

when I saw this problem I figured it was going to be reduced to SAT. truly the swiss army knife of algorithms

[@quintonpierre]

Is there any reference about this new look-ahead strategy?

[@OpPhilo03]

5-6 days ago i was thinking about that and today you have make this video😂😂. I am surprise😂

[@eclipse1353]

The explanation of S(k) is quite unambiguous, since we could assume a can or cannot be equal to b. so, 1 could be color 1, 2 cannot be formed with 1 1 so it can be color 1, 3=1+2 so it has to be color 2, etc. if a and b had to be distinct numbers, S(k) would be a lot larger. so, S(1)=2, S(2)>=7, S(3)>16 these results are just with a greedy algorithm. I´m quite sure S(4)>>44

[@romangeneral23]

I feel like mathematicians come up with the most random things they can think of and convince everyone that it is fundamental to something that they also made up...

[@conanedojawa4538]

What if the condition a+b=c be subtraction or multiplication?

[@wv1seahawks]

See the way I think of this problem is TOTALLY different haha. Because if you have a number where a+b=c must be monochromatic, then every a,b pair are the same color. In the case of 14, I can do 1+13, 2+12, 3+11,…. This means that when I have a number that cannot satisfy this property, then the coloring of the preceding numbers has a reflection. So for 5 it goes b,y|y,b and for 14 it goes b,y,y,b,p,p|b|p,p,b,y,y,b. So like I wonder if it is faster computationally to just brute force color them and when you detect a possible reflection, you can estimate what the solution could be. Instead of running this massive proof for each case of n

[@matthewsarsam8920]

Great video

[@WingMyWay]

Things like the ABC conjecture prove that you dont need length for proofs to be tedious.

[@georgehaas7292]

I love how he says “Bruce Force” instead of “Brute Force” 😂

[@DrTrefor]

Ha, I heard this in editing and was like “nobody is going to notice right? Right???”🤣

[@georgehaas7292]

I love your video though! Just thought it was kinda funny

[@straft5759]

Bruce Force is when you hire a mathematician called Bruce to solve the problem for you

[@perplexedon9834]

I was watching through this and though "wow this is a neat problem, I can't wait to see what genius insight makes this proof obvious" and then I remembered that the proof involves petabytes of brute force lmao

[@SlimThrull]

Hm... This seems very similar to the Three Color Problem in graph theory. I'm curious is you could represent this problem as a graph and solve it that way.

[@petrikor]

if it has a mapping reduction to SAT, then i dont see why not

[@erickehr4475]

If they had applied this method to the case of 160 numbers, would it have actually found a solution, or just declared that a solution was possible?

[@ZoranRavic]

I assume it would log the solution. We do know of some solutions already.

[@HagenvonEitzen]

The video assigned yellow to 3 and blue to 1. For additional math video nerd points , I would instead have coloured 3 blue, 1 brown.

[@ennocramer4703]

So what now is Schur(6) ?

[@DrTrefor]

Please no I can’t even

[@tsuwako7497]

No one knows yet but I think the current upper and lower bounds are 535 < S(6) < 1928

[@dentonyoung4314]

And I thought the proof of the four-color theorem was long...

[@beautifulsmall]

the up arrow is A or else B, you didnt explain that for us softies who use other similarly bizzare notation.

[@pallharaldsson9015]

16:32 "2 terabyte-size proof", I think you misspoke, i.e. it's 1000 times larger, you already mentioned 2 PB proof. [I see you confirmed this in another comment.] Could edit the video?

[@GeoffryGifari]

Are the proof-making and proof-verification done without humans on the loop? How can mathematicians know that the verification is valid?

[@Kataquax]

By having a formal verification of the software that checks/verifies the proof

[@anmolkaushal5892]

Sir, Please do cover Riemann Steiltjes integral.

[@markshiman5690]

How did they brute force 160 back then?

[@DrTrefor]

Some symmetries and cleverness let them find the example without brute forcing it. The brute force method eventually found all the millions of examples that work for 160, but the first is actually a palindrome

[@isbestlizard]

It's a very unsatisfying proof though. The best proofs (imo) link the problem to some other area of mathematics and lead to new insight or methods. This is just brute forcing a load of CPU cycles and doesn't advance maths in any way.

[@DrTrefor]

I partly see this, but personally I still found HOW they computed it and the way they encoded and then simplified the encoding to be tractable still had some interest. That said, a lot of this is aesthetic so to each their own!

[@AbelShields]

I think some problems are just more akin to engineering than maths. Some maths problems can easily be generalised and proofs for those may lead us to new and interesting ideas. But I think some problems, you just get the answer, yes or no, and that's it. I'm not sure any alternative proof to this would give us any new insights - is there some deeper truth to the lack of 5-colourability in a 161-node graph that's connected in a very particular way? I don't think so.

[@IOverlord]

"Unsasitfying" Sounds like a human problem

[@isbestlizard]

@@IOverlord It would be so cool if we meet aliens and exchange maths knowledge! Discovering what overlap, what theorems and proofs we've independently discovered and in what order, whether either of us have missed something 'obvious' and get that forehead-slap moment when we share it. Like, do aliens know about the fast fourier transform? :D

[@Nnm26]

@@isbestlizardthat is assuming math is a concept to them

[@JohnDlugosz]

I seem to have missed the actual result that was found. What is S(5)?

[@DrTrefor]

160

[@LilacShowers]

great video, but what's wrong with your mic? it sounds really bad

[@abc24601]

Lucky them that 161 couldn’t be colored. If the program had identified a coloring scheme, 162 could’ve been intractable.

[@rodrigoqteixeira]

Bro I know lookahead saves time but damn it's so hard... (I'm entering 13-14 sec zone tho, so it's working) #cubing #lookahead #speedcubing

[@WilliamTaylor-h4r]

It was just teasing you while it proved levitation was possible with the other 15 robot years.

[@mohannad_139]

Since someone found the minimum value of S(5) in 90s and it turned to be the answer, isn't it the time to find the minimum value of S(6)?

[@DrTrefor]

Good luck!!!!

[@mohannad_139]

@@DrTrefor Nah I'm not doing it 💀

[@purplenanite]

I got a 481 but i know that's not anywhere near the limit

[@quay6292]

Why does this sounds very similar to abc-conjecture?

[@gregorymorse8423]

I don't think this is the largest proof. Kolmogorov complexity of compressing the algorithm that generated those numbers is the proof. In fact proof lengths are very hard to compare unless you prove it minimal even then based upon a certain set of postulates and axioms. Expanding out an algorithm and calling that a proof would make chasing the longest algorithm with nonsense problems trivial. Also you cannot prove the hardware worked accurately so easily. So it is hard to call it a proof without some sort of proof certificate and even then verifying the certificate is also on hardware that could have faults. It is rather a proof with some provably high probability which should be scientifically calculated. Anyway I don't buy that the algorithm isn't the proof. But this is an interesting question. E.g. meta proof concept. But minimal form can be objectively formed even if intractable

[@freshrockpapa-e7799]

And how does the verifying algorithm work? That seems even more interesting

[@JohnDoe-ti2np]

To a first approximation, the 2 petabyte file is just a "trace" (i.e., a complete transcript) of the SAT solver computation, so the verifying algorithm just retraces the steps of the original computation. That's not quite right, though, because they use some clever tricks to write down a correctness proof efficiently (something called a DRAT proof of unsatisfiability). But the time required to verify the proof is still on the same order of magnitude as generating the proof in the first place.

[@freshrockpapa-e7799]

@@JohnDoe-ti2np So they just do the same thing twice? Why is that required to verify the problem?

[@JohnDoe-ti2np]

@@freshrockpapa-e7799 The difference is that the first time around, the program generates a 2 petabyte file, and the second time around, a separate program (or a separate part of the program) goes through the 2 petabyte file and confirms that it is correct. Confirming the correctness of the 2 petabyte file can be done with a much simpler computer program than the program that was used to generate the file in the first place; the 2 petabyte file has a certain standard format, and in principle a third party can write their own program to verify it. Compare this with the "old-fashioned" procedure of just running a very complicated program for a huge amount of time and having it declare "There is no solution" at the end, with no further supporting evidence. The 2 petabyte file functions as a "certificate" that a skeptical auditor can validate after the fact, using a simple program that is much less likely to have bugs than a large and complicated piece of software.

[@JohnDoe-ti2np]

@@freshrockpapa-e7799 The difference is that the first time around, the program *generates* the 2 petabyte proof that the system has no solution, but the second time around, a separate program *checks* the proof. The proof follows a simple, standard format, so checking the proof can be accomplished with a much simpler (and therefore less bug-prone) program. The checking program can even be written by a third-party "auditor". For comparison, imagine a complicated program running for days on a kajillion computers and then just printing out, "There is no solution" with no corroborating evidence for its verdict. The 2 petabyte file serves as a "certificate" that can be straightforwardly validated (although of course it still takes a long time to sift through 2 petabtyes).

[@JohnDoe-ti2np]

@@freshrockpapa-e7799 The difference is that the first time around, the program *generates* the 2 petabyte proof that the system has no solution, but the second time around, a separate program *checks* the proof. The proof follows a simple, standard format, so checking the proof can be accomplished with a much simpler (and therefore less bug-prone) program. The checking program can even be written by a third-party "auditor".

[@59de44955ebd]

When I hear something like "14 CPU years" I can't help, I have to think about climate change and the immense energy consumption that such a rather secondary mathematical proof required. At the times of Euler or Fermat, a proof caused no energy consumption at all, other than maybe a few candles burned at night. And given that our little planet is so fragile and already in bad shape, I wonder if that's really the right way to advance in math (and science in general).

[@59de44955ebd]

ps: the same applies to the largest known mersenne prime number that was recently found. Finding it doesn't help at all in getting a deeper understanding of the prime distribution, but propably caused a carbon emission in the order of the consumption of a small town in a few days. Does this really make sense?

[@DrTrefor]

I hear that for sure, but also this video has been watched for about 220 days continuously so far. Ok that isn’t 14 years, but a more popular KZbinr would be watched that amount. Food for thought.

[@Kreypossukr]

This is so cool

[@aberone_library]

At first I thought this was gonna be about the finite simple group classification haha

[@DrTrefor]

Ha yes that’s a different measure of “longest proof” for sure

[@MrVontar]

161-11=150/5=30. 11+2=13, and 1+13+30=44. 160/5=15/5=3, which is stopping it from reaching 161. Maybe 169 lol.

[@MrVontar]

Err, actually I think it is 200. Not sure tho, this problem seems kind of silly

[@MrVontar]

This is actually simple..If no a,b,c =same color then there must always be a variable that is a negation of the other states for each series possible. If that is not possible, then it has no solution.

[@MrVontar]

Also idk why you are saying the solution isn't satisfied when 1 is yellow too, all you do is flip the other states around. This seems like a pretty trivial problem but I may be misunderstanding it

[@MrVontar]

It is kind of like proving an infinite numbers of primes. Let 1+1=2. Then 2+2=4. Let half of a number exist, this is half of 2 and half of 4, which is 3. Then any number constructed must be a prime eventually since half of the numbers up to 4 are prime and all numbers mod 4 will be bounded by the initial construct of the number line then every number series must eventually generate a new prime since all other numbers can be generated by the recursive operation over the initial states. By induction, unless numbers are not number then there must be an infinite amount of primes due to the theorem of arithmetic so it is also trivial in a way.

[@NStripleseven]

wtf are you talking about

[@rodrigoqteixeira]

5:45 nah bud, you can assume the number 1 color and completely remove that same color from number 2. That reduces the amout of options 6.25 times.

[@paulamarina04]

well yeah, thats what the solver does, on a much larger scale

[@jamesharmon4994]

I thought for sure he was talking about the proof that 1+ 1 = 2. I'm serious.

[@DrTrefor]

Haha I almost put in an reference to this 😂

[@MorgurEdits]

Did you mean GPU instead of CPU? sounds like a problem GPU's could shine in.

[@RabbitInAHumanWoild]

Thanks for an interesting video. Have you ever considered the cost in tonnes of carbon dioxide released while doing computations like this?

[@DrTrefor]

i don't even want to!

[@RabbitInAHumanWoild]

@@DrTrefor To be clear, I was not being glib. This was a serious question as these supercomputers are being used for for more things, especially AI. We are now at the point where questions like mine need to be asked.

[@Kreypossukr]

So basically SAT solvers are the ultimate proofs by exhaustion machines

[@DrTrefor]

They are insanely powerful, but still tonnes of things that are way to big for them to be useful

[@janisir4529]

Problems like these tend to be NP, so they'll take exponential time to compute, SAT solvers just make it less bad.

[@MadScientyst]

& Here I thought Fermat's Theorem & proof was complicated enough. Now here comes another (kinda Number Theory) wonder to blow Brain cells! 🤔

[@asparkdeity8717]

given even checking takes up so much computational power, do we need to then verify the verification of the proof, and then verify that, and then verify that etc.. 😂

[@michaelleue7594]

So I'm curious if the proof also established classes of solutions for coloring 160 numbers. Obviously there are at least 5! ways to do it that are just swapping the colors of the same solution around, but are there more than that? What colorings of the first 5 numbers lead to solutions, and what colorings are dead ends?

[@DrTrefor]

Yes, the details are in the paper but he computes the precise number of satisfied cases and it is more than the 5! trivial permutations.

[@davidmaes3253]

You lose me directly at the start. @1:15 you state that "you'll notice that we get a bunch of tripples". I see that. But why is that? What is the rule or premise to change from one color to another?

[@6AxisSage]

mathematics proofs will all look like this eventually because the whole concept is so stupid but everyone in charge makes all their money with this circus.

[@JorgetePanete]

The audio is weird, at least in mono.

[@JorgetePanete]

The video is also laggy.

[@christopherlocke]

Do you also need statements to ensure that each number cannot have more than one color? For example (p^b and not p^y) or (not p^b and p^y)?

[@gdclemo]

Probably not, as a solution where a number has multiple colors just proves that it can be either. This is because, as I understand it, aside from the expressions that check that every number has at least one color, all the other expressions depend on the negative, i.e a number not being a particular color, rather than having to be a particular color. Though it may speed up the SAT solver to add those statements as you might be able to eliminate the possibility of multiple colors more quickly.

[@christopherlocke]

@@gdclemo Makes sense, thanks!

[@bambangnugroho6147]

The colors making problematic life.

[@maxmusterman3371]

Very nice video. Amazing how such proofs are possible wow. Humanity has come so far being able to use ~30 cpu years to proof such a (sry) random fact 😂

[@DrTrefor]

ha fair probably people were not thinking in the 70s we would be spending our incredible computer abilities on....uh....this:D

[@Bruno_Noobador]

Spoiler: the answer was 7

[@finxy3500]

9:12 should be xor or equivalent I think.

[@DrTrefor]

there's a detail I didn't include in the video which is that you should as you suggest ALSO do something to eliminate the possibility one number gets multiple colours - the authors add separate regular or statements for that, but then do some symmetry breaking tricks to simplify again so I just glossed over all of this for the sake of (20 minutes?) brevity.

[@ThatJudahvr]

Just 2 peta bytes

[@WilliametcCook]

Ladies and gentlemen, this is S(5)

[@xwtek3505]

Hearing that the proof uses SAT makes me disappointed, lol

[@DrTrefor]

Ha fair BUT what if I said it was a rather clever use of sat solvers:D

[@xwtek3505]

@@DrTrefor Not really. If I hear a problem that goes "here is the possible solution space and here are the constrants (that is efficently computable in polynomial time)" my first instinct is "use SAT". It's basically brute force but more efficient

[@Be-lo_da_fluff]

why not have every odd number as blue? odd+odd=even

[@Be-lo_da_fluff]

also i think the schur number of 3 is >13 but im doing this in my head rn and might have made a mistake

[@ZoranRavic]

You could put all odd numbers in blue, but then you end up needing more colors for the even numbers. For example if you have 3 colors and 13 numbers, you can't put all odd numbers in the same color, but if you mix the numbers you can find a solution. Trying to put all odd numbers together could be useful to get an approximate lower bound, although most researcher use a more complicated template when trying combinations.

[@Absorpy]

You should probably get a new mic