För ungefär tio år sedan bevisade Marijn Heule, Oliver Kullmann och Victor Marek att om man 2-färgar de positiva heltalen från 1 till 7825, så måste man kunna hitta x, y och z som alla har samma färg med x^2+y^2=z^2 -- det vill säga en monokromatisk pythagoreisk trippel. 1/

Detta löste ett gammalt problem med Ron Graham. Beviset var ett massivt brute-force-argument. Inte ren brute force, eftersom det skulle ha varit helt ogenomförbart, utan en smart brute-force-beräkning med hjälp av en SAT-lösare. 2/

Men jag är ganska säker på att det var humoristiskt menat och inte (som föreslogs i Quanta-artikeln) som någon form av kritik, eftersom jag tror nu, och tänkte då, att den här typen av resultat är ganska coola. 4/

Skämtet skulle ha varit att man skulle kunna läsa ett bevis av den här typen som om det vore en mer konventionell typ av argumentation, och komplicerade kasusanalyser i konventionella argument anses i allmänhet vara något fula. 5/

Men ett bevis av det här slaget är naturligtvis inte utformat för att läsas på det konventionella sättet, och har sin egen typ av dragningskraft. Personligen är jag okej med tanken på att använda trevliga argument för att reducera ett bevis till en massiv beräkning och sedan göra beräkningen. 6/

Det verkar finnas vissa problem som realistiskt sett inte kan lösas på annat sätt än genom den här typen av tillvägagångssätt, i vilket fall jag inte ser någon anledning att inte använda det, och jag är nöjd med den resulterande nivån av förståelse. 7/

Med det sagt, om någon skulle hitta ett bevis för fyrfärgssatsen (till exempel) som inte krävde en stor fallanalys, skulle jag fira det och betrakta det som ett framsteg i förståelse, eftersom det skulle förklara varför fallanalysen hade fungerat.

vilket jag för närvarande betraktar som något som bara råkar vara fallet. På samma sätt, om någon skulle hitta ett argument i mänsklig skala för Pythagoras-tripplingproblemet så skulle jag bli förtjust. Men jag tvivlar starkt på att ett sådant argument existerar, och det stör mig inte. 9/9