339:
as the 4-color theorem and the Kepler conjecture, use long computer calculations as well as many pages of mathematical argument. For the computer calculations in this section, the mathematical arguments are only a few pages long, and the length is due to long but routine calculations. Some typical examples of such theorems include:
338:
There are many mathematical theorems that have been checked by long computer calculations. If these were written out as proofs many would be far longer than most of the proofs above. There is not really a clear distinction between computer calculations and proofs, as several of the proofs above, such
465:
is provable in Peano arithmetic but the shortest proof has at least a googolplex symbols. It has a short proof in a more powerful system: in fact, it is easily provable in Peano arithmetic together with the statement that Peano arithmetic is consistent (which cannot be proved in Peano arithmetic by
268:. Perelman's original proofs of the Poincaré conjecture and the Geometrization conjecture were not lengthy, but were rather sketchy. Several other mathematicians have published proofs with the details filled in, which come to several hundred pages.
146:
on finitely generated infinite groups with finite exponents negatively. The three-part original paper is more than 300 pages long. (Britton later published a 282-page paper attempting to solve the problem, but his paper contained a serious
168:. Grothendieck's work on the foundations of algebraic geometry covers many thousands of pages. Although this is not a proof of a single theorem, there are several theorems in it whose proofs depend on hundreds of earlier pages.
355:, the computer proofs were later replaced by shorter proofs avoiding computer calculations. Similarly, the calculation of the maximal subgroups of the larger sporadic groups uses a lot of computer calculations.
131:. Harish-Chandra's construction of these involved a long series of papers totaling around 500 pages. His later work on the Plancherel theorem for semisimple groups added another 150 pages to these.
473:
In this argument, Peano arithmetic can be replaced by any more powerful consistent system, and a googolplex can be replaced by any number that can be described concisely in the system.
479:
found some explicit natural examples of this phenomenon, giving some explicit statements in Peano arithmetic and other formal systems whose shortest proofs are ridiculously long (
54:
The length of unusually long proofs has increased with time. As a rough rule of thumb, 100 pages in 1900, or 200 pages in 1950, or 500 pages in 2000 is unusually long for a proof.
222:. Gorenstein and Lyons's proof for the case of rank at least 4 was 731 pages long, and Aschbacher's proof of the rank 3 case adds another 159 pages, for a total of 890 pages.
457:
showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is absurdly long. For example, the statement:
46:
with well over 10000 pages. There are several proofs that would be far longer than this if the details of the computer calculations they depend on were published in full.
282:. The proof of this is spread out over hundreds of journal articles which makes it hard to estimate its total length, which is probably around 10000 to 20000 pages.
421:
of the length 1161 has a discrepancy at least 3; the original proof, generated by a SAT solver, had a size of 13 gigabytes and was later reduced to 850 megabytes.
106:
by Feit and
Thompson was 255 pages long, which at the time was over 10 times as long as what had previously been considered a long paper in group theory.
190:. While Deligne's final paper proving these conjectures were "only" about 30 pages long, it depended on background results in algebraic geometry and
275:. The classification of the simple quasithin groups by Aschbacher and Smith was 1221 pages long, one of the longest single papers ever written.
158:
120:
for 3-folds in characteristic greater than 6 covered about 500 pages in several papers. In 2009, Cutkosky simplified this to about 40 pages.
164:
583:"Two-hundred-terabyte maths proof is largest ever: A computer cracks the Boolean Pythagorean triples problem — but is it really maths?"
152:
351:, originally used computer calculations with large matrices or with permutations on billions of symbols. In most cases, such as the
300:'s proof of this involves several hundred pages of published arguments, together with several gigabytes of computer calculations.
175:. Thompson's classification of N-groups used 6 papers totaling about 400 pages, but also used earlier results of his such as the
279:
43:
652:
390:
467:
425:
229:. Hejhal's proof of a general form of the Selberg trace formula consisted of 2 volumes with a total length of 1322 pages.
17:
714:
582:
113:. Hironaka's original proof was 216 pages long; it has since been simplified considerably down to about 10 or 20 pages.
435:, who coauthored solution to the Boolean Pythagorean triples problem, announced a 2 petabytes long proof that the 5th
232:
239:
312:
124:
449:
286:
205:
63:
724:
320:
316:
304:
404:
117:
110:
96:
535:
is provable in Peano arithmetic, but the shortest proof has length at least 2, where 2 = 1 and 2 = 2 (
235:. Arthur's proofs of the various versions of this cover several hundred pages spread over many papers.
556:
265:
261:
59:
201:. Appel and Haken's proof of this took 139 pages, and also depended on long computer calculations.
42:
As of 2011, the longest mathematical proof, measured by number of published journal pages, is the
544:
74:
32:
344:
297:
246:
257:
561:
363:
325:
226:
143:
73:
1890 Killing's classification of simple complex Lie algebras, including his discovery of the
690:
662:
540:
183:
85:
36:
8:
253:'s proof of this was about 600 pages long, not counting many pages of background results.
215:. Langlands's proof of the functional equation for Eisenstein series was 337 pages long.
191:
694:
604:
461:"This statement cannot be proved in Peano arithmetic in less than a googolplex symbols"
436:
359:
352:
219:
28:
99:
took 98 pages, but has since been simplified: modern proofs are less than a page long.
719:
698:
648:
293:
250:
212:
176:
103:
67:
678:
640:
623:
377:
308:
187:
686:
658:
636:
528:
476:
387:
272:
198:
172:
627:
249:
on the
Langlands conjecture for the general linear group over function fields.
92:
644:
418:
414:
407:: Every odd number greater than 5 can be expressed as the sum of three primes.
708:
135:
454:
411:
66:, but his proof, spanning 500 pages, was mostly ignored and later, in 1824,
600:
432:
208:
classifying finite groups of sectional 2-rank at most 4 was 464 pages long.
139:
536:
348:
682:
629:
The proof is in the pudding. The changing nature of mathematical proof
128:
81:
609:
370:
397:
669:
Smoryński, C. (1982), "The varieties of arboreal experience",
289:. The proof takes about 500 pages spread over about 20 papers.
179:, which bring to total length up to more than 700 pages.
527:+10 vertices, then some tree can be homeomorphically
443:
194:
that
Deligne estimated to be about 2000 pages long.
428:required the generation of 200 terabytes of proof.
491:such that if there is a sequence of rooted trees
706:
70:published a proof that required just six pages.
383:Calculations of large numbers of digits of π.
333:
80:1894 The ruler-and-compass construction of a
539:growth). The statement is a special case of
668:
608:
480:
380:with around ten million digits are prime.
323:. The paper comprised 180 pages in the
14:
707:
622:
280:Classification of finite simple groups
44:classification of finite simple groups
599:
242:. Almgren's proof was 955 pages long.
153:Fondements de la Géometrie Algébrique
580:
426:Boolean Pythagorean triples problem
417:for the particular case C=2: every
343:Several proofs of the existence of
24:
25:
736:
444:Long proofs in mathematical logic
165:Séminaire de géométrie algébrique
27:This is a list of unusually long
159:Éléments de géométrie algébrique
396:2012 Showing that Sudoku needs
125:Discrete series representations
593:
574:
483:). For example, the statement
468:Gödel's incompleteness theorem
362:for the first 10 zeros of the
49:
13:
1:
603:(2017). "Schur Number Five".
567:
77:, took 180 pages in 4 papers.
581:Lamb, Evelyn (26 May 2016).
305:strong perfect graph theorem
240:Almgren's regularity theorem
233:Arthur–Selberg trace formula
7:
550:
405:Ternary Goldbach conjecture
118:resolution of singularities
111:Resolution of singularities
33:computational proof methods
10:
741:
447:
334:Long computer calculations
116:1966 Abyhankar's proof of
715:Mathematics-related lists
645:10.1007/978-0-387-48744-1
557:List of incomplete proofs
543:and has a short proof in
391:can be solved in 20 moves
376:2008 Proofs that various
358:2004 Verification of the
287:Robertson–Seymour theorem
266:Geometrization conjecture
206:Gorenstein–Harada theorem
95:'s original proof of the
450:Gödel's speed-up theorem
75:exceptional Lie algebras
31:. Such proofs often use
545:second order arithmetic
369:2007 Verification that
415:discrepancy conjecture
386:2010 Showing that the
345:sporadic simple groups
262:Geometrization theorem
97:Lasker–Noether theorem
82:polygon of 65537 sides
35:and may be considered
562:Proof by intimidation
487:"there is an integer
364:Riemann zeta function
326:Annals of Mathematics
227:Selberg trace formula
62:was nearly proved by
635:, Berlin, New York:
184:Ramanujan conjecture
88:took over 200 pages.
86:Johann Gustav Hermes
60:Abel–Ruffini theorem
725:Mathematical proofs
671:Math. Intelligencer
601:Heule, Marijn J. H.
258:Poincaré conjecture
247:Lafforgue's theorem
29:mathematical proofs
18:List of long proofs
683:10.1007/bf03023553
360:Riemann hypothesis
353:baby monster group
220:Trichotomy theorem
144:Burnside's problem
654:978-0-387-48908-7
624:Krantz, Steven G.
541:Kruskal's theorem
424:2016 Solving the
398:at least 17 clues
294:Kepler conjecture
251:Laurent Lafforgue
213:Eisenstein series
177:odd order theorem
104:Odd order theorem
68:Niels Henrik Abel
16:(Redirected from
732:
701:
665:
634:
615:
614:
612:
597:
591:
590:
578:
378:Mersenne numbers
309:Maria Chudnovsky
273:Quasithin groups
192:Ă©tale cohomology
188:Weil conjectures
21:
740:
739:
735:
734:
733:
731:
730:
729:
705:
704:
655:
637:Springer-Verlag
632:
619:
618:
598:
594:
579:
575:
570:
553:
531:in a later one"
522:
513:
504:
497:
477:Harvey Friedman
452:
446:
336:
199:4-color theorem
173:N-group theorem
52:
23:
22:
15:
12:
11:
5:
738:
728:
727:
722:
717:
703:
702:
677:(4): 182–189,
666:
653:
617:
616:
592:
572:
571:
569:
566:
565:
564:
559:
552:
549:
533:
532:
518:
509:
502:
495:
481:Smoryński 1982
463:
462:
448:Main article:
445:
442:
441:
440:
437:Schur's number
429:
422:
410:2014 Proof of
408:
401:
394:
384:
381:
374:
367:
356:
347:, such as the
335:
332:
331:
330:
313:Neil Robertson
301:
290:
283:
276:
269:
254:
243:
236:
230:
223:
216:
209:
202:
195:
180:
169:
148:
142:proof solving
132:
121:
114:
107:
100:
93:Emanuel Lasker
89:
78:
71:
51:
48:
37:non-surveyable
9:
6:
4:
3:
2:
737:
726:
723:
721:
718:
716:
713:
712:
710:
700:
696:
692:
688:
684:
680:
676:
672:
667:
664:
660:
656:
650:
646:
642:
638:
631:
630:
625:
621:
620:
611:
606:
602:
596:
588:
584:
577:
573:
563:
560:
558:
555:
554:
548:
546:
542:
538:
530:
526:
521:
517:
512:
508:
501:
494:
490:
486:
485:
484:
482:
478:
474:
471:
469:
460:
459:
458:
456:
451:
438:
434:
430:
427:
423:
420:
416:
413:
409:
406:
402:
399:
395:
392:
389:
385:
382:
379:
375:
372:
368:
365:
361:
357:
354:
350:
346:
342:
341:
340:
328:
327:
322:
318:
314:
310:
306:
302:
299:
295:
291:
288:
284:
281:
277:
274:
270:
267:
263:
259:
255:
252:
248:
244:
241:
237:
234:
231:
228:
224:
221:
217:
214:
210:
207:
203:
200:
196:
193:
189:
185:
181:
178:
174:
170:
167:
166:
161:
160:
155:
154:
149:
145:
141:
137:
133:
130:
126:
122:
119:
115:
112:
108:
105:
101:
98:
94:
90:
87:
83:
79:
76:
72:
69:
65:
64:Paolo Ruffini
61:
57:
56:
55:
47:
45:
40:
38:
34:
30:
19:
674:
670:
628:
595:
586:
576:
534:
524:
523:has at most
519:
515:
510:
506:
499:
492:
488:
475:
472:
464:
453:
433:Marijn Heule
388:Rubik's Cube
337:
324:
321:Robin Thomas
317:Paul Seymour
163:
157:
151:
53:
41:
26:
537:tetrational
419:±1-sequence
349:Lyons group
50:Long proofs
709:Categories
610:1711.08076
568:References
514:such that
455:Kurt Gödel
373:is a draw.
150:1960-1970
129:Lie groups
699:125748405
303:2006 the
204:1974 The
134:1968 the
58:1799 The
720:Theorems
626:(2011),
551:See also
529:embedded
371:checkers
186:and the
691:0685558
663:2789493
505:, ...,
439:is 161.
136:Novikov
697:
689:
661:
651:
587:Nature
319:, and
695:S2CID
633:(PDF)
605:arXiv
431:2017
412:Erdős
403:2013
307:, by
298:Hales
292:2005
285:2004
278:2004
271:2004
256:2003
245:2000
238:2000
225:1983
218:1983
211:1976
197:1974
182:1974
171:1974
147:gap.)
140:Adian
123:1966
109:1964
102:1963
91:1905
649:ISBN
162:and
679:doi
641:doi
470:).
127:of
84:by
711::
693:,
687:MR
685:,
673:,
659:MR
657:,
647:,
639:,
585:.
547:.
498:,
315:,
311:,
296:.
264:,
260:,
156:,
39:.
681::
675:4
643::
613:.
607::
589:.
525:k
520:k
516:T
511:n
507:T
503:2
500:T
496:1
493:T
489:n
400:.
393:.
366:.
329:.
138:–
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.