From 4d5bc9ecd0701510cb6aecf9a634fa3b82d4ec11 Mon Sep 17 00:00:00 2001 From: bixbyr Date: Sun, 19 Jul 2026 14:44:20 -0700 Subject: [PATCH 1/3] feat: Add Shafarevich's Theorem on solvable Galois groups problem Co-authored-by: Gemini 3.1 Pro --- LeanEval.lean | 1 + LeanEval/NumberTheory/Shafarevich.lean | 15 +++++++++++++++ manifests/problems/shafarevich.toml | 9 +++++++++ 3 files changed, 25 insertions(+) create mode 100644 LeanEval/NumberTheory/Shafarevich.lean create mode 100644 manifests/problems/shafarevich.toml diff --git a/LeanEval.lean b/LeanEval.lean index a5ae96df..467c1d1f 100644 --- a/LeanEval.lean +++ b/LeanEval.lean @@ -16,3 +16,4 @@ import LeanEval.NumberTheory.SmallHouse import LeanEval.Topology.CerfGammaFour import LeanEval.Topology.HomotopyGroups import LeanEval.Topology.SmaleConjecture +import LeanEval.NumberTheory.Shafarevich diff --git a/LeanEval/NumberTheory/Shafarevich.lean b/LeanEval/NumberTheory/Shafarevich.lean new file mode 100644 index 00000000..c711c3e4 --- /dev/null +++ b/LeanEval/NumberTheory/Shafarevich.lean @@ -0,0 +1,15 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace NumberTheory + +/-- **Shafarevich's Theorem**. Every finite solvable group is realizable as a Galois group over `ℚ`. -/ +@[eval_problem] +theorem shafarevich (G : Type*) [Group G] [Finite G] [IsSolvable G] : + ∃ (K : Type*) (_ : Field K) (_ : Algebra ℚ K) (_ : FiniteDimensional ℚ K) (_ : IsGalois ℚ K), + Nonempty (G ≃* (K ≃ₐ[ℚ] K)) := by + sorry + +end NumberTheory +end LeanEval diff --git a/manifests/problems/shafarevich.toml b/manifests/problems/shafarevich.toml new file mode 100644 index 00000000..2f987d4c --- /dev/null +++ b/manifests/problems/shafarevich.toml @@ -0,0 +1,9 @@ +id = "shafarevich" +title = "Shafarevich's Theorem on Solvable Galois Groups" +test = false +module = "LeanEval.NumberTheory.Shafarevich" +holes = ["shafarevich"] +submitter = "Ryan Smith" +notes = "Every finite solvable group is realizable as a Galois group over \u211a." +source = "Shafarevich, I. R. (1954). On the construction of fields with a given Galois group of order l^a. Izvestiya Akademii Nauk SSSR. For modern book-length treatments and simplified proofs, see Malle, G., & Matzat, B. H. (1999). 'Inverse Galois Theory' (Springer Monographs in Mathematics), Chapter II. Also see Neukirch, J., Schmidt, A., & Wingberg, K. (2008). 'Cohomology of Number Fields' (Grundlehren der mathematischen Wissenschaften 323, Springer)." +informal_solution = "Construct the extension inductively by lifting the solvable group along a composition series, using the fact that every step is an abelian extension. The obstruction to the embedding problem at each step is resolved using Scholz's theorem or Neukirch's cohomological methods to ensure the local behavior at ramified primes allows the extension." From 0d490c94a5f3c08b03deb3b852c25c94c1fb27f1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 30 Jul 2026 12:00:56 +0000 Subject: [PATCH 2/3] chore(NumberTheory): disambiguate the Shafarevich problem and clean up Rename to shafarevich_solvable_galois: a bare `shafarevich` collides in readers' heads with shafarevich_relation_rank_bound and golod_shafarevich_inequality. Existential field in `Type` rather than `Type*`, matching the other realizability problems, so a solver isn't obliged to ULift. Drop the LeanEval.lean import, which aggregates only a handful of problem modules and conflicts with the sibling PRs. Expand notes to say what Mathlib does and doesn't provide. Co-Authored-By: Claude Opus 5 (1M context) --- LeanEval.lean | 1 - LeanEval/NumberTheory/Shafarevich.lean | 15 --------------- .../NumberTheory/ShafarevichSolvableGalois.lean | 16 ++++++++++++++++ ...ich.toml => shafarevich_solvable_galois.toml} | 10 +++++----- 4 files changed, 21 insertions(+), 21 deletions(-) delete mode 100644 LeanEval/NumberTheory/Shafarevich.lean create mode 100644 LeanEval/NumberTheory/ShafarevichSolvableGalois.lean rename manifests/problems/{shafarevich.toml => shafarevich_solvable_galois.toml} (50%) diff --git a/LeanEval.lean b/LeanEval.lean index 467c1d1f..a5ae96df 100644 --- a/LeanEval.lean +++ b/LeanEval.lean @@ -16,4 +16,3 @@ import LeanEval.NumberTheory.SmallHouse import LeanEval.Topology.CerfGammaFour import LeanEval.Topology.HomotopyGroups import LeanEval.Topology.SmaleConjecture -import LeanEval.NumberTheory.Shafarevich diff --git a/LeanEval/NumberTheory/Shafarevich.lean b/LeanEval/NumberTheory/Shafarevich.lean deleted file mode 100644 index c711c3e4..00000000 --- a/LeanEval/NumberTheory/Shafarevich.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Mathlib -import EvalTools.Markers - -namespace LeanEval -namespace NumberTheory - -/-- **Shafarevich's Theorem**. Every finite solvable group is realizable as a Galois group over `ℚ`. -/ -@[eval_problem] -theorem shafarevich (G : Type*) [Group G] [Finite G] [IsSolvable G] : - ∃ (K : Type*) (_ : Field K) (_ : Algebra ℚ K) (_ : FiniteDimensional ℚ K) (_ : IsGalois ℚ K), - Nonempty (G ≃* (K ≃ₐ[ℚ] K)) := by - sorry - -end NumberTheory -end LeanEval diff --git a/LeanEval/NumberTheory/ShafarevichSolvableGalois.lean b/LeanEval/NumberTheory/ShafarevichSolvableGalois.lean new file mode 100644 index 00000000..ce3a2c50 --- /dev/null +++ b/LeanEval/NumberTheory/ShafarevichSolvableGalois.lean @@ -0,0 +1,16 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace NumberTheory + +/-- **Shafarevich's theorem on solvable Galois groups**. Every finite solvable +group is realizable as a Galois group over `ℚ`. -/ +@[eval_problem] +theorem shafarevich_solvable_galois (G : Type*) [Group G] [Finite G] [IsSolvable G] : + ∃ (K : Type) (_ : Field K) (_ : Algebra ℚ K) (_ : FiniteDimensional ℚ K) (_ : IsGalois ℚ K), + Nonempty (G ≃* (K ≃ₐ[ℚ] K)) := by + sorry + +end NumberTheory +end LeanEval diff --git a/manifests/problems/shafarevich.toml b/manifests/problems/shafarevich_solvable_galois.toml similarity index 50% rename from manifests/problems/shafarevich.toml rename to manifests/problems/shafarevich_solvable_galois.toml index 2f987d4c..54f7814c 100644 --- a/manifests/problems/shafarevich.toml +++ b/manifests/problems/shafarevich_solvable_galois.toml @@ -1,9 +1,9 @@ -id = "shafarevich" -title = "Shafarevich's Theorem on Solvable Galois Groups" +id = "shafarevich_solvable_galois" +title = "Shafarevich's theorem on solvable Galois groups" test = false -module = "LeanEval.NumberTheory.Shafarevich" -holes = ["shafarevich"] +module = "LeanEval.NumberTheory.ShafarevichSolvableGalois" +holes = ["shafarevich_solvable_galois"] submitter = "Ryan Smith" -notes = "Every finite solvable group is realizable as a Galois group over \u211a." +notes = "Every finite solvable group is realizable as a Galois group over ℚ: the solvable case of the inverse Galois problem. Mathlib has IsSolvable and the Galois correspondence, but nothing about realizability — no embedding problems, no Scholz–Reichardt construction, no inverse-Galois API at all — so a solver builds the extensions from scratch. Distinct from the two other Shafarevich problems in the catalog: shafarevich_relation_rank_bound (the cohomological relation-rank inequality for the maximal unramified pro-p extension) and golod_shafarevich_inequality. Note that Shafarevich's original 1954 argument had an error at the prime 2, repaired later; the statement here is the corrected theorem, as treated in the Malle–Matzat and Neukirch–Schmidt–Wingberg references below." source = "Shafarevich, I. R. (1954). On the construction of fields with a given Galois group of order l^a. Izvestiya Akademii Nauk SSSR. For modern book-length treatments and simplified proofs, see Malle, G., & Matzat, B. H. (1999). 'Inverse Galois Theory' (Springer Monographs in Mathematics), Chapter II. Also see Neukirch, J., Schmidt, A., & Wingberg, K. (2008). 'Cohomology of Number Fields' (Grundlehren der mathematischen Wissenschaften 323, Springer)." informal_solution = "Construct the extension inductively by lifting the solvable group along a composition series, using the fact that every step is an abelian extension. The obstruction to the embedding problem at each step is resolved using Scholz's theorem or Neukirch's cohomological methods to ensure the local behavior at ramified primes allows the extension." From e497039d06e1c5fa6417071ee12c3d5be15b2942 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 30 Jul 2026 12:01:57 +0000 Subject: [PATCH 3/3] docs: correct Shafarevich theorem sources --- manifests/problems/shafarevich_solvable_galois.toml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/manifests/problems/shafarevich_solvable_galois.toml b/manifests/problems/shafarevich_solvable_galois.toml index 54f7814c..ed0c4189 100644 --- a/manifests/problems/shafarevich_solvable_galois.toml +++ b/manifests/problems/shafarevich_solvable_galois.toml @@ -4,6 +4,6 @@ test = false module = "LeanEval.NumberTheory.ShafarevichSolvableGalois" holes = ["shafarevich_solvable_galois"] submitter = "Ryan Smith" -notes = "Every finite solvable group is realizable as a Galois group over ℚ: the solvable case of the inverse Galois problem. Mathlib has IsSolvable and the Galois correspondence, but nothing about realizability — no embedding problems, no Scholz–Reichardt construction, no inverse-Galois API at all — so a solver builds the extensions from scratch. Distinct from the two other Shafarevich problems in the catalog: shafarevich_relation_rank_bound (the cohomological relation-rank inequality for the maximal unramified pro-p extension) and golod_shafarevich_inequality. Note that Shafarevich's original 1954 argument had an error at the prime 2, repaired later; the statement here is the corrected theorem, as treated in the Malle–Matzat and Neukirch–Schmidt–Wingberg references below." -source = "Shafarevich, I. R. (1954). On the construction of fields with a given Galois group of order l^a. Izvestiya Akademii Nauk SSSR. For modern book-length treatments and simplified proofs, see Malle, G., & Matzat, B. H. (1999). 'Inverse Galois Theory' (Springer Monographs in Mathematics), Chapter II. Also see Neukirch, J., Schmidt, A., & Wingberg, K. (2008). 'Cohomology of Number Fields' (Grundlehren der mathematischen Wissenschaften 323, Springer)." -informal_solution = "Construct the extension inductively by lifting the solvable group along a composition series, using the fact that every step is an abelian extension. The obstruction to the embedding problem at each step is resolved using Scholz's theorem or Neukirch's cohomological methods to ensure the local behavior at ramified primes allows the extension." +notes = "Every finite solvable group is realizable as a Galois group over ℚ: the solvable case of the inverse Galois problem. Mathlib has IsSolvable and the Galois correspondence, but nothing about realizability — no embedding problems, no Scholz–Reichardt construction, no inverse-Galois API at all — so a solver builds the extensions from scratch. Distinct from the two other Shafarevich problems in the catalog: shafarevich_relation_rank_bound (the cohomological relation-rank inequality for the maximal unramified pro-p extension) and golod_shafarevich_inequality. Shafarevich's original 1954 proof contained an error at the prime 2, which he later corrected; the source field cites both the correction and a modern complete proof." +source = "I. R. Shafarevich, 'Construction of fields of algebraic numbers with given solvable Galois group', Izv. Akad. Nauk SSSR Ser. Mat. 18 (1954), no. 6, 525–578, https://www.mathnet.ru/eng/im3517. The prime-2 correction appears in Shafarevich's Collected Mathematical Papers, Springer (1989). For a complete corrected proof, see A. Schmidt and K. Wingberg, 'Šafarevič's theorem on solvable groups as Galois groups' (1998), https://arxiv.org/abs/math/9809211." +informal_solution = "Reduce the realization problem to split finite embedding problems with nilpotent kernels. For each p-primary kernel, construct controlled Scholz solutions and solve successive central embedding problems. When an obstruction appears, Shafarevich's shrinking procedure modifies earlier stages so that the obstruction vanishes; the corrected argument handles the prime 2. Iterating along a solvable series yields a finite Galois extension K/ℚ with Galois group G."