นี่คือรายชื่อบทพิสูจน์ทางคณิตศาสตร์ ที่ยาวผิดปกติ บทพิสูจน์เหล่านี้มักใช้วิธีการพิสูจน์เชิงคำนวณและอาจถือได้ว่าไม่สามารถตรวจสอบได้ด้วยวิธีสำรวจ

ณ ปี 2011 บทพิสูจน์ทางคณิตศาสตร์ที่ยาวที่สุด วัดจากจำนวนหน้าในวารสารที่ตีพิมพ์ คือการจำแนกกลุ่มง่ายจำกัดซึ่งมีจำนวนหน้ามากกว่า 10,000 หน้า นอกจากนี้ยังมีบทพิสูจน์อีกหลายชิ้นที่จะยาวกว่านี้มาก หากรายละเอียดของการคำนวณด้วยคอมพิวเตอร์ที่ใช้เป็นพื้นฐานได้รับการตีพิมพ์อย่างครบถ้วน

ความยาวของเอกสารพิสูจน์อักษรที่ยาวผิดปกติได้เพิ่มขึ้นตามกาลเวลา โดยประมาณแล้ว เอกสารพิสูจน์อักษรที่ยาว 100 หน้าในปี 1900 หรือ 200 หน้าในปี 1950 หรือ 500 หน้าในปี 2000 ถือว่ายาวผิดปกติ

• ปี 1799 – เปาโล รัฟฟิ นี เกือบจะพิสูจน์ทฤษฎีบทอาเบล-รัฟฟินี ได้สำเร็จ แต่บทพิสูจน์ของเขาซึ่งมีความยาวถึง 500 หน้า กลับถูกละเลยเป็นส่วนใหญ่ และต่อมาในปี 1824 นีลส์ เฮนริก อาเบลได้ตีพิมพ์บทพิสูจน์ที่ใช้เพียงหกหน้าเท่านั้น
• ปี 1890 – การจำแนกประเภทของพีชคณิตลีเชิงซ้อนแบบง่าย ของ คิลลิงซึ่งรวมถึงการค้นพบพีชคณิตลีแบบพิเศษ ของเขา ใช้เวลาถึง 180 หน้า ใน 4 บทความ
• ปี 1894 – การสร้างรูป หลายเหลี่ยมที่มี 65,537 ด้านโดยใช้ไม้บรรทัดและวงเวียนโดยโยฮันน์ กุสตาฟ เฮอร์เมสใช้เวลานานมากกว่า 200 หน้า
• ปี 1905 – การพิสูจน์ทฤษฎีบท ลาสเกอร์ -โนเธอ ร์ฉบับดั้งเดิมของเอ็มมานูเอล ลาสเกอร์ใช้เวลาถึง 98 หน้า แต่ต่อมาได้มีการทำให้ง่ายขึ้น โดยการพิสูจน์ในปัจจุบันใช้เวลาน้อยกว่าหนึ่งหน้า
• ปี 1963 – ทฤษฎีบทลำดับคี่ ของเฟตและทอม ป์สันมีความยาว 255 หน้า ซึ่งในขณะนั้นยาวกว่าบทความวิจัยที่ยาวที่สุดในทฤษฎีกลุ่ม ถึงกว่า 10 เท่า
• ปี 1964 – การแก้ปัญหาภาวะเอกฐานบทพิสูจน์ดั้งเดิมของฮิโรนากะมีความยาว 216 หน้า แต่ต่อมาได้มีการลดทอนให้เหลือเพียงประมาณ 10 หรือ 20 หน้า
• ปี 1966 – บทพิสูจน์ของ Abyhankar เกี่ยวกับการแก้ปัญหาภาวะเอกฐานสำหรับ 3-folds ที่มีลักษณะเฉพาะมากกว่า 6 นั้นครอบคลุมประมาณ 500 หน้าในเอกสารหลายฉบับ ในปี 2009 Cutkosky ได้ย่อให้เหลือเพียงประมาณ 40 หน้า
• ปี 1966 – การ แสดง กลุ่มลีด้วยอนุกรมแบบไม่ต่อเนื่องการสร้างอนุกรมเหล่านี้ของฮาริช-จันทราเกี่ยวข้องกับเอกสารจำนวนมากรวมประมาณ 500 หน้า งานต่อมาของเขาเกี่ยวกับทฤษฎีบทแพลนเชอเรลสำหรับกลุ่มกึ่งง่ายได้เพิ่มอีก 150 หน้าเข้าไปในเอกสารเหล่านั้น
• ปี 1968 – การพิสูจน์ของ โนวิคอฟ - เอเดียนที่แก้ปัญหาของเบิร์นไซด์เกี่ยวกับกลุ่มอนันต์ที่สร้างขึ้นอย่างจำกัด และมี เลขชี้กำลัง จำกัด เป็นลบ บทความต้นฉบับสามส่วนมีความยาวมากกว่า 300 หน้า (ต่อมาบริตตันได้ตีพิมพ์บทความ 282 หน้าที่พยายามแก้ปัญหานี้ แต่บทความของเขามีช่องว่างที่สำคัญ)
• ปี 1960-1970 – Fondements de la Géometrie Algébrique , Éléments de géométrie algébriqueและSéminaire de géométrie algébriqueผลงานของ Grothendieck เกี่ยวกับพื้นฐานของเรขาคณิตเชิงพีชคณิตครอบคลุมหลายพันหน้า แม้ว่านี่จะไม่ใช่การพิสูจน์ทฤษฎีบทเดียว แต่ก็มีทฤษฎีบทหลายข้อในนั้นที่การพิสูจน์ขึ้นอยู่กับงานหลายร้อยหน้าก่อนหน้านี้
• ปี 1974 – ทฤษฎีบทกลุ่ม Nการจำแนกกลุ่ม N ของทอมป์สันใช้เอกสาร 6 ฉบับ รวมประมาณ 400 หน้า แต่ยังใช้ผลลัพธ์ก่อนหน้านี้ของเขา เช่นทฤษฎีบทอันดับคี่ซึ่งทำให้ความยาวรวมเพิ่มขึ้นเป็นมากกว่า 700 หน้า
• ปี 1974 – ข้อสันนิษฐานของรามานุจันและข้อสันนิษฐานของไวล์แม้ว่าบทความฉบับสุดท้ายของเดลิญที่พิสูจน์ข้อสันนิษฐานเหล่านี้จะมีความยาว "เพียง" ประมาณ 30 หน้า แต่ก็ต้องอาศัยผลลัพธ์พื้นฐานในเรขาคณิตเชิงพีชคณิตและเอทาลโคฮอโมโลยีซึ่งเดลิญประเมินว่ามีความยาวประมาณ 2,000 หน้า
• ปี 1974 – ทฤษฎีบทสี่สีการพิสูจน์ของแอปเปลและฮาเคนใช้เวลาถึง 139 หน้า และยังต้องอาศัยการคำนวณด้วยคอมพิวเตอร์เป็นเวลานานอีกด้วย
• ปี 1974 – ทฤษฎีบท Gorenstein–Haradaซึ่งจำแนกกลุ่มจำกัดที่มีอันดับภาคตัดขวาง 2 ไม่เกิน 4 มีความยาว 464 หน้า
• ปี 1976 – อนุกรมไอเซนสไตน์บทพิสูจน์สมการเชิงฟังก์ชันสำหรับอนุกรมไอเซนสไตน์ของแลงแลนด์ มีความยาวถึง 337 หน้า
• ปี 1983 – ทฤษฎีบทไตรภาค (Trichotomy theorem ) บทพิสูจน์ของโกเรนสไตน์และไลออนส์สำหรับกรณีอันดับอย่างน้อย 4 มีความยาว 731 หน้า และบทพิสูจน์ของแอชบาเชอร์สำหรับกรณีอันดับ 3 เพิ่มอีก 159 หน้า รวมเป็น 890 หน้า
• 1983 – สูตรร่องรอยเซลเบิร์กการพิสูจน์สูตรร่องรอยเซลเบิร์กในรูปแบบทั่วไปของเฮจฮาลประกอบด้วย 2 เล่ม รวมทั้งหมด 1322 หน้า
• สูตรร่องรอยของอาร์เธอร์-เซลเบิร์กบทพิสูจน์ของอาร์เธอร์เกี่ยวกับสูตรนี้ในหลายเวอร์ชันครอบคลุมหลายร้อยหน้าและกระจายอยู่ในเอกสารหลายฉบับ
• ปี 2000 – ทฤษฎีความสม่ำเสมอของอัลม์เกรนบทพิสูจน์ของอัลม์เกรนมีความยาว 955 หน้า
• ปี 2000 – ทฤษฎีบทของลาฟฟอร์กเกี่ยวกับการคาดการณ์ของแลงแลนด์สำหรับกลุ่มเชิงเส้นทั่วไปเหนือฟิลด์ฟังก์ชัน การพิสูจน์ของ ลอรองต์ ลาฟฟอร์กนั้นยาวประมาณ 600 หน้า ไม่รวมผลลัพธ์เบื้องหลังอีกหลายหน้า
• ปี 2003 – ข้อสันนิฐานของปวงกาเร , ทฤษฎีบทเรขาคณิต , ข้อสันนิฐานเรขาคณิตบทพิสูจน์ดั้งเดิมของเพอร์แมนน์เกี่ยวกับข้อสันนิฐานของปวงกาเรและข้อสันนิฐานเรขาคณิตนั้นไม่ยาวนัก แต่ค่อนข้างคร่าวๆ นักคณิตศาสตร์คนอื่นๆ อีกหลายคนได้ตีพิมพ์บทพิสูจน์ที่มีรายละเอียดครบถ้วน ซึ่งมีความยาวหลายร้อยหน้า
• ปี 2004 – กลุ่มควาซิธินการจำแนก กลุ่มควาซิธิน อย่างง่ายโดย Aschbacher และ Smith มีความยาวถึง 1221 หน้า ซึ่งเป็นหนึ่งในบทความวิจัยที่ยาวที่สุดเท่าที่เคยเขียนมา
• ปี 2004 – การจำแนกกลุ่มง่ายจำกัดการพิสูจน์เรื่องนี้กระจายอยู่ในบทความวารสารหลายร้อยฉบับ ทำให้ยากที่จะประมาณความยาวทั้งหมด ซึ่งน่าจะอยู่ที่ประมาณ 10,000 ถึง 20,000 หน้า
• ปี 2004 – ทฤษฎีบทโรเบิร์ตสัน-เซย์มัวร์การพิสูจน์ใช้เวลาประมาณ 500 หน้า โดยแบ่งออกเป็นประมาณ 20 บทความ
• ปี 2005 – สมมติฐานของเคปเลอร์การ พิสูจน์ของ เฮลส์ในเรื่องนี้ประกอบด้วยข้อโต้แย้งที่ตีพิมพ์หลายร้อยหน้า พร้อมด้วยการคำนวณด้วยคอมพิวเตอร์หลายกิกะไบต์
• ปี 2006 – ทฤษฎีบทกราฟสมบูรณ์แบบที่แข็งแกร่งโดยมาเรีย ชูดนอฟสกี , นีล โรเบิร์ตสัน , พอล ซีมัวร์และโรบิน โทมัสบทความนี้มีความยาว 180 หน้า ตีพิมพ์ในวารสารAnnals of Mathematics

มีทฤษฎีบททางคณิตศาสตร์มากมายที่ได้รับการตรวจสอบแล้วด้วยการคำนวณด้วยคอมพิวเตอร์ที่ยาวนาน หากเขียนออกมาเป็นบทพิสูจน์ หลายบทพิสูจน์จะยาวกว่าบทพิสูจน์ส่วนใหญ่ข้างต้นมาก จริงๆ แล้วไม่มีเส้นแบ่งที่ชัดเจนระหว่างการคำนวณด้วยคอมพิวเตอร์และบทพิสูจน์ เนื่องจากบทพิสูจน์หลายบทข้างต้น เช่น ทฤษฎีบทสี่สีและข้อสันนิษฐานของเคปเลอร์ ใช้การคำนวณด้วยคอมพิวเตอร์ที่ยาวนาน รวมถึงการอธิบายทางคณิตศาสตร์หลายหน้า สำหรับการคำนวณด้วยคอมพิวเตอร์ในส่วนนี้ การอธิบายทางคณิตศาสตร์มีความยาวเพียงไม่กี่หน้า และความยาวนั้นเกิดจากการคำนวณที่ยาวนานแต่เป็นขั้นตอนปกติ ตัวอย่างทั่วไปของทฤษฎีบทดังกล่าว ได้แก่:

• การพิสูจน์การมีอยู่ของกลุ่มง่ายแบบสปอราดิก หลายกลุ่ม เช่นกลุ่มไลออนส์เดิมทีใช้การคำนวณด้วยคอมพิวเตอร์โดยใช้เมทริกซ์ ขนาดใหญ่ หรือการเรียงสับเปลี่ยนบนสัญลักษณ์หลายพันล้านตัว ในกรณีส่วนใหญ่ เช่นกลุ่มเบบี้มอนสเตอร์ การพิสูจน์ด้วยคอมพิวเตอร์ถูกแทนที่ด้วยการพิสูจน์ที่สั้นกว่าซึ่งหลีกเลี่ยงการคำนวณด้วยคอมพิวเตอร์ในภายหลัง ในทำนองเดียวกัน การคำนวณกลุ่มย่อยสูงสุดของกลุ่มสปอราดิกขนาดใหญ่ก็ใช้การคำนวณด้วยคอมพิวเตอร์จำนวนมาก เช่นกัน
• การพิสูจน์ว่าจำนวนใดจำนวนหนึ่งเป็นจำนวน เฉพาะ
• 2004 – การตรวจสอบสมมติฐานของรีมันน์ สำหรับศูนย์ ^10¹³ ตัวแรกของฟังก์ชันซีตาของรีมันน์
• ปี 2007 – ยืนยันว่าเกมหมากรุกจบลงด้วยผลเสมอ
• การคำนวณค่า πที่มีจำนวนมากหลัก
• ปี 2010 – แสดงให้เห็นว่าสามารถแก้ลูกรูบิค ได้ภายใน 20 ขั้น ตอน
• ปี 2012 – พิสูจน์ให้เห็นว่าซูโดกุต้องใช้คำใบ้อย่างน้อย 17คำ
• ปี 2013 – ทฤษฎีบทโกลด์บัคแบบไตรภาค : จำนวน คี่ ทุก จำนวนที่มากกว่า 5 สามารถแสดงได้ในรูปผลรวมของจำนวนเฉพาะสามจำนวน
• 2014 – การพิสูจน์ข้อสันนิษฐานความคลาดเคลื่อน ของ Erdős สำหรับกรณีเฉพาะC = 2: ลำดับ ±1 ทุกลำดับที่มีความยาว 1161 มีความคลาดเคลื่อนอย่างน้อย 3; หลักฐานการพิสูจน์ดั้งเดิมซึ่งสร้างขึ้นโดยโปรแกรมแก้ปัญหา SATมีขนาด 13 กิกะไบต์ และต่อมาได้ลดขนาดลงเหลือ 850 เมกะไบต์
• 2016 – การแก้ปัญหาสามเหลี่ยมพีทาโกเรียนบูลีนต้องใช้การสร้างหลักฐานขนาด 200 เทราไบต์^{[ 1 ]}
• 2017 – Marijn Heuleผู้ร่วมเขียนวิธีแก้ปัญหา Boolean Pythagorean triples ประกาศการพิสูจน์ความยาว 2 เพตาไบต์ว่าเลข Schur ที่ 5 คือ 160 ^{[ 2 ]}

เคิร์ท เกอเดลได้แสดงให้เห็นถึงวิธีการค้นหาตัวอย่างที่ชัดเจนของข้อความในระบบที่เป็นทางการ ซึ่งสามารถพิสูจน์ได้ในระบบนั้น แต่การพิสูจน์ ที่สั้นที่สุด กลับยาวเหยียดอย่างไม่น่าเชื่อ ตัวอย่างเช่น ข้อความที่ว่า:

"ข้อความนี้ไม่สามารถพิสูจน์ได้ด้วยเลขคณิตของพีอาโนโดยใช้สัญลักษณ์น้อยกว่ากูเกิลเพล็กซ์ "

สามารถพิสูจน์ได้ในเลขคณิตของพีอาโน แต่การพิสูจน์ที่สั้นที่สุดต้องใช้สัญลักษณ์อย่างน้อยกูเกิลเพล็กซ์ มีการพิสูจน์ที่สั้นกว่าในระบบที่มีประสิทธิภาพมากกว่า: อันที่จริง สามารถพิสูจน์ได้ง่ายในเลขคณิตของพีอาโน พร้อมกับข้อความที่ว่าเลขคณิตของพีอาโนมีความสอดคล้อง (ซึ่งไม่สามารถพิสูจน์ได้ในเลขคณิตของพีอาโนโดยทฤษฎีบทความไม่สมบูรณ์ของเกอเดล )

ในข้อโต้แย้งนี้ เลขคณิตของพีอาโนสามารถแทนที่ด้วยระบบที่มีประสิทธิภาพและสอดคล้องกันมากกว่าได้ และกูเกิลเพล็กซ์สามารถแทนที่ด้วยจำนวนใดๆ ก็ได้ที่สามารถอธิบายได้อย่างกระชับในระบบนั้น

ฮาร์วีย์ ฟรีดแมนพบตัวอย่างทางธรรมชาติที่ชัดเจนของปรากฏการณ์นี้ โดยให้ข้อความที่ชัดเจนบางประการในเลขคณิตของพีอาโนและระบบที่เป็นทางการอื่นๆ ซึ่งการพิสูจน์ที่สั้นที่สุดนั้นยาวเหยียดอย่างไม่น่าเชื่อ ( Smoryński 1982 ) ตัวอย่างเช่น ข้อความดังกล่าว

"มีจำนวนเต็มn อยู่จำนวนหนึ่ง ซึ่งถ้ามีลำดับของต้นไม้รากT ₁ , T ₂ , ..., T _nโดยที่T _kมีจุดยอดไม่เกินk +10 จุด แล้ว ต้นไม้บางต้นสามารถฝัง ตัวแบบโฮมีโอเมอร์ฟิก ในต้นไม้ต้นถัดไปได้"

สามารถพิสูจน์ได้ด้วยเลขคณิตของ Peano แต่การพิสูจน์ที่สั้นที่สุดมีความยาวอย่างน้อย¹⁰⁰⁰ 2 โดยที่⁰ 2 = 1 และ^{n +1} 2 = 2 ^{( n 2)} ( การเติบโต แบบเททราชันนัล ) ข้อความนี้เป็นกรณีพิเศษของทฤษฎีบทของ Kruskalและมีการพิสูจน์สั้นๆ ด้วยเลขคณิตอันดับสอง

• รายชื่อบทพิสูจน์ที่ไม่สมบูรณ์
• หลักฐานโดยการข่มขู่