odd-order-submission

日本語版

This repository packages a self-contained Lean 4 submission of the Feit–Thompson odd-order theorem for the feit_thompson challenge in leanprover/lean-eval.

Important

This is an extracted submission snapshot, not the canonical development repository. It was produced from the completed odd-order repository, which is planned for public release. The exact source revision and toolchain are recorded in SOURCE_LOCK.json.

The theorem

The Feit–Thompson theorem states that every finite group of odd order is solvable. The challenge is presented in Lean as:

theorem feit_thompson {G : Type*} [Group G] [Finite G]
    (_h : Odd (Nat.card G)) : IsSolvable G

feit_thompson/Submission.lean connects this challenge declaration to the extracted proof of OddOrder.feitThompson.

What this repository provides

The proof was completed in the upstream odd-order development repository. This repository focuses on turning that proof into a reproducible, self-contained lean-eval submission:

• the 588-module local import closure needed by OddOrder.feitThompson;
• the fixed lean-eval challenge scaffold and submission adapter;
• deterministic extraction, slicing, and provenance checks;
• dependency and source-reference inventories used to retain everything needed for safe re-elaboration;
• measurements from clean builds, export, comparator validation, and Lean kernel replay.

The extraction does not conceal or rebrand the source. Logical names remain in the OddOrder.* namespace, source attribution is retained, and only physical module imports are re-rooted under Submission.OddOrder.*. The final theorem-only slice conservatively removes unused plain theorem and lemma commands while preserving definitions, instances, notation, attributes, structural commands, and elaboration-time dependencies.

Repository layout

Path	Role
feit_thompson/	Fixed challenge scaffold and final submission
feit_thompson/Submission.lean	Submission entry point
feit_thompson/Submission/OddOrder/	Extracted proof modules
SOURCE_LOCK.json	Upstream revision, toolchain pins, and dependency counts
scripts/	Extraction, slice generation, integrity checks, and local evaluation harness
tools/	Lean-based dependency and source-reference inventory tooling
measurements/	Recorded build, export, replay, and size results
SUBMISSION_STRATEGY.md	Detailed extraction and validation rationale (Japanese)

Pinned snapshot

Item	Value
Upstream project	Completed odd-order repository (public release planned)
Upstream commit	92e9199344a4163ded9662aabe3e217ab445e0a7
Lean	v4.32.0-rc1
Mathlib	360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56
Entry module	OddOrder.FeitThompson
Target declaration	OddOrder.feitThompson
Extracted modules	588
Final manifest SHA-256	9401f23b29adcc50dd03ba33d5e216a24ba82e6e80a928fb044cb9fc8e7bbd66

The current candidate has passed a clean build, the permitted-axiom check, the pinned lean4export pipeline, the lean-eval comparator, and replay by Lean's default kernel. The resulting theorem uses only propext, Classical.choice, and Quot.sound, matching the challenge's permitted axiom set. The repository's Python test suite contains 31 passing tests.

Verification

The repository-level checks that do not require the upstream checkout are:

python3 -m unittest discover -s tests -v
python3 scripts/check_scaffold_integrity.py
sha256sum feit_thompson/Submission/OddOrder.manifest.json

With the pinned Lean and Mathlib dependencies available, build the submitted solution from the challenge workspace:

cd feit_thompson
lake build Solution

lake test additionally runs the comparator and therefore requires a comparator binary in PATH or in COMPARATOR_BIN. For a fail-closed local reproduction of the exporter/comparator workflow, see scripts/run_local_eval_harness.sh and the Japanese README.

Reproducing the extraction

To verify provenance or regenerate the slice, check out the completed upstream repository as ../odd-order at the pinned commit. The source-lock check requires that checkout to be clean:

python3 scripts/check_source_lock.py

A dry run of the full import-closure extraction is available with:

python3 scripts/extract_feit_thompson.py \
  --source-root ../odd-order \
  --expect-count 588 \
  --dry-run

The theorem-only v2 slice is generated from the pinned inventories. Generated files under feit_thompson/Submission/OddOrder/ should not be edited by hand; regenerate them from the locked source and inventories instead. See SUBMISSION_STRATEGY.md and tools/README.md for the complete workflow.

Resource notes

The v2 slice reduces the normalized source archive by 7.42% and generated .olean data by 8.56% relative to the full import-closure baseline. It does not claim a clean-build speedup: the recorded single run was 5.13% slower, while peak build memory changed by only -0.71%. Final export remains about 1.03 GB and export/replay peaks at about 7.40 GiB of memory. Raw results and their limitations are preserved under measurements/.

License

This repository is licensed under the Apache License 2.0.