FLT10bench Q10: Frey package construction

Proved

FLT10Bench.q10_of_counterexample

by Jin Gao · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

fltflt10benchnumber-theory

Let $a,b,c\in\mathbb Z$ be nonzero integers, let $p\in\mathbb N$ be prime with $p\ge 5$ , and assume

a^p+b^p=c^p.

Then a Frey package exists for this putative counterexample. The package records nonzero integer data, a prime exponent at least $5$ , the Fermat equation, and the standard normalization data used in the Frey-curve construction: $\gcd(a,b)=1$ , $a\equiv 3\pmod 4$ , and $b\equiv 0\pmod 2$ . It also provides the associated integral and rational Frey curves. This is the first (Q10) checkpoint of FLT10bench and supplies the Frey-package object used by the later irreducibility, modularity, and level-lowering checkpoints.

Formalization Note The conclusion is expressed by the Lean type $\mathrm{Nonempty}\ \mathrm{FreyPackage}$ , where $\mathrm{FreyPackage}$ is the structure defined by the FLT preliminary development.

Preamble

import Mathlib
import Definitions.Def_FLTPrelim_FreyPackage

set_option autoImplicit false
set_option maxHeartbeats 4000000
set_option synthInstance.maxHeartbeats 400000
set_option backward.isDefEq.respectTransparency.types false

Formal statement

theorem FLT10Bench.q10_of_counterexample (a b c : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (p : ℕ) (pp : p.Prime) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FreyPackage := by sorry

Source

https://github.com/shiyegao/ContextSwarm-ICLR/blob/2450835c06914330ebfd099fd94ddd0924ac5bab/benchmarks/FLT10bench/flt10_q10_of_counterexample/problem.md (FLT10bench Q10; canonical source theorem FreyPackage.of_counterexample: https://github.com/anthropics/fermats-last-theorem/blob/2226972cf818e220d16da6683474496664a6fc67/Theorems/Thm_FreyPackage_of_counterexample.lean)

View graph