在Lean正规化的有限简易团体分类

中文版正在随流水线自动整理，稍后刷新即可；可先阅读下方英文原文。

本文由 AI图鉴自动抓取并翻译，版权归原作者所有；如需查看原文请点下方链接。

Mathematics that came out of the formalization. More papers will appear here.

The Unbalanced Group Theorem

Hexagon 2610.00575 · 35 pages

A new group theory result that came out of this formalization project is reported in this paper. While formalizing the first-generation proof, we found counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem. The paper explains the obstruction and gives an alternative argument for the simple-group case, built on Solomon’s 1976 theory of maximal 2-components, whose key step is Theorem 2.3, the preservation of simple tops.

We are working with group theorists to compile the errata we found in the literature, and will publish them here.

Zoom in to read each statement

The Classification of Finite Simple Groups, formalized in Lean

The classification of finite simple groups is one of the great collective achievements of mathematics. Its first-generation proof spans thousands of journal pages, written by about a hundred mathematicians over several decades. It shows that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups.

Here we present a complete formalization in Lean following the first-generation proof, with every logical step checked by Lean’s kernel. Along the way, we found an issue in a published argument for the Unbalanced Group Theorem. The accompanying paper explains the issue and the alternative route used in our proof. Our blog post tells the full story.

Other contributorsRafael Cabral†, Colin Defant*, Erik Gregory†, Aaron Hill†, Letong Hong◇, Qinheping Hu†, Dustin Jamner†, Albert Jiang†, Tadeusz Jordan†, Andranik Kurghinyan†, Kenny Lau*†, Jonathan Laurent†, David Liang†, Jannis Limperg†, Simon Mahns†, Brian Nugent*, Connor Olson†, Ken Ono*, Eric Paul†, Dhruv Rajan†, Karun Ram†, Charlie Ray†, Ho Chung Siu†, Ashvin A. Swaminathan*†, Jesse Thorner*, Aleksey Tsaplin†, Chenkai Wang†

Auto-fetched and translated by AI Atlas. All rights belong to the original author.