---
type: "post"
id: "selected-departures-from-published-arguments-in-the-classification-d64eb4"
slug: "selected-departures-from-published-arguments-in-the-classification-d64eb4"
title: "Selected Departures from Published Arguments in the Classification of Finite Simple Groups"
description: "Axiom Math’s 28 October 2026 document records 96 selected departures found while formalizing the classification of finite simple groups in Lean."
retrieval_nugget: "Axiom Math’s 28 October 2026 document records 96 selected departures found while formalizing the classification of finite simple groups in Lean. It says AxiomProver produced the listed corrections and alternative arguments, while stressing that the entries are neither a count of errors nor a challenge to the classification itself."
published_at: "2026-11-06"
updated_at: "2026-11-06"
record_date: "2026-11-06"
date_kind: "published_at"
topics: ["verification"]
entities: ["Axiom Math","AxiomProver","Lean","Classification of finite simple groups"]
related_patterns: ["scientific-agents-need-artifact-evidence"]
novelty_label: "new_fact"
what_changed: "Axiom Math’s errata document records 96 selected departures from published CFSG arguments, including corrected statements and alternative proof steps; it stresses these do not challenge the theorem."
prior_refs: []
source_url: "https://cfsg.axiommath.ai/CFSG_errata.pdf"
source_urls: ["https://cfsg.axiommath.ai/CFSG_errata.pdf"]
schema_version: "newruntime-agent-readable-v0.2"
stable_id: "post:selected-departures-from-published-arguments-in-the-classification-d64eb4"
status: "published"
visuals: []
editor: {"role":"editor","name":"Andrey Reshetnikov","profile":"https://newruntime.com/owner-profile.md","profile_json":"https://newruntime.com/owner-profile.json","same_as":["https://www.linkedin.com/in/reshetnikov1/","https://t.me/lapetuse"]}
routes: {"html":"https://newruntime.com/posts/selected-departures-from-published-arguments-in-the-classification-d64eb4/","markdown":"https://newruntime.com/posts/selected-departures-from-published-arguments-in-the-classification-d64eb4.md","json":"https://newruntime.com/posts/selected-departures-from-published-arguments-in-the-classification-d64eb4.json"}
markdown_url: "https://newruntime.com/posts/selected-departures-from-published-arguments-in-the-classification-d64eb4.md"
---

# Selected Departures from Published Arguments in the Classification of Finite Simple Groups

## Retrieval answer

Axiom Math’s 28 October 2026 document records 96 selected departures found while formalizing the classification of finite simple groups in Lean. It says AxiomProver produced the listed corrections and alternative arguments, while stressing that the entries are neither a count of errors nor a challenge to the classification itself.

## Summary
Axiom Math’s 28 October 2026 document records 96 selected departures found while formalizing the classification of finite simple groups in Lean. It says AxiomProver produced the listed corrections and alternative arguments, while stressing that the entries are neither a count of errors nor a challenge to the classification itself.

## What happened
Axiom Math published *Selected Departures from Published Arguments: Notes on the formalization of the classification of finite simple groups*. The document accompanies its Lean formalization of the classification of finite simple groups (CFSG), a theorem it describes as correct and as one of mathematics’ great collective achievements. Its subject is not the theorem’s validity, but particular supporting statements and proof steps in the first-generation proof and related literature.

The document contains 96 selected mathematical departures and elaborations. Axiom Math divides them into Part A, with 34 entries on structural changes and alternative proofs, and Part B, with 62 entries on additional arguments and local corrections. The categories describe the extent of the change to an argument, not the seriousness of an error or the mathematical importance of a result. The selection is not comprehensive: routine typographical corrections, notational changes, and readily repaired slips are omitted. Related consequences of one difficulty may be grouped together.

The entries include counterexamples to particular auxiliary assertions, omitted cases in lists, supplementary arguments, and replacements for proof steps that retain an intended conclusion. Some cases invalidate an intermediate inference without meeting every hypothesis of the surrounding theorem. In some instances, the formalization obtains a more restricted statement sufficient for the classification, rather than recovering a stronger printed assertion in its original generality. The document says it identifies relevant statements, sources and page references where available; it is intended for mathematicians reading those sources.

One example in the supplied material concerns the relative *ZJ* theorem in a 1970 work by Alperin, Brauer and Gorenstein. Axiom Math gives a counterexample to the printed unrestricted statement, then says the application instead uses a relative result with an explicit Frattini condition. Another entry addresses statements in Aschbacher’s 1981 work: the document says an omitted degree-two case defeats two assertions as printed, while a version with added conditions is used in the formalization. These examples illustrate the document’s distinction between correcting a local route through the literature and disputing CFSG itself.

Axiom Math attributes the recorded corrections, supplementary arguments and alternative proofs to its AI system AxiomProver, which produced them during the formalization. It explicitly does not claim priority for every correction or underlying idea: some were already known. The introduction points to Case 1 as an alternative argument concerning the Unbalanced Group Theorem and a closure issue in Walter’s memoir. The supplied document excerpt identifies the scope and organization of the list, but does not establish independent expert review of each entry, public availability of the complete formal artifact, or quantify how much of the formalization was automated.

## What the archive adds
This is a new fact on the broader story of formal proof systems finding and checking mathematical arguments. Our [AlphaProof Nexus note](https://newruntime.com/posts/google-deepmind-s-alphaproof-nexus-solved-9-open-07c5ac/) covered open Erdos problems and machine-checkable proof obligations; our [EasyProver note](https://newruntime.com/posts/easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9/) covered Lean proving results and a Rust-to-Lean benchmark. The present document adds a specific audit trail of changes to arguments in a major existing proof.

## Trend signal
This supports the pattern that [scientific agents need artifact evidence](https://newruntime.com/patterns/scientific-agents-need-artifact-evidence/). Formalization can expose where a proof depends on a statement or inference that needs correction, restriction or an alternate argument, but the useful evidence is the inspectable account of those changes rather than a broad capability claim. It also fits the archive’s [analysis of three AI proof claims](https://newruntime.com/analysis/research-of-three-ai-proof-claims-only-the-qcd-proof-is-unreleased-eth-and-cfsg-await/), which distinguishes the CFSG claim from the evidence needed to assess it.

## Why it matters
For teams building AI systems for mathematics or other high-stakes technical work, the useful output is not simply a model’s assertion that it solved a problem. A formal artifact can make individual claims checkable, while a carefully scoped errata document makes disagreements legible: readers can see which supporting claim changed, what replacement argument is offered, and whether the final theorem is affected.

Axiom Math’s own caveats are essential to interpreting the number 96. It is a curated set of departures, not a failure count, novelty count, or measure of model capability. The case suggests a better standard for reporting automated research: identify the exact artifact, cite the source being examined, distinguish previously known material from new work, and state whether the central result survives. That standard helps researchers evaluate contribution without conflating formal verification with discovery.

## Limits and uncertainty
The document is Axiom Math’s account of its own formalization. The supplied material does not provide an independent assessment of all 96 entries, a comparison of the full Lean code with each cited source, or evidence about the time and human effort required. It says some corrections were already known and makes no priority claim for every item. The list is explicitly selective, and some entries concern author-manuscript versions. Nothing here shows that CFSG is false: the document says the classification is correct and that its listed departures concern supporting statements and proof steps.

## Reader takeaway
The headline number is 96 selected departures, not 96 errors or discoveries. The important result is narrower: Axiom Math says its Lean formalization, with corrections attributed to AxiomProver, identified specific places where supporting arguments could be corrected, supplemented or replaced without calling the classification into question.

Editor: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Verification](https://newruntime.com/topics/verification.md): Explore the verification topic hub.
- collection: [Field Notes](https://newruntime.com/posts.json): Open the latest editorial analysis.
- collection: [Sources](https://newruntime.com/sources/): See the original sources this archive cites.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)