Repository navigation

Integrate eight reviewed formalization projects - #467

Merged

Vilin97 merged 141 commits into

mainfrom

feature/reviewed-imports-20260921

Sep 21, 2026

Merged

Integrate eight reviewed formalization projects#467
Vilin97 merged 141 commits into
mainfrom
feature/reviewed-imports-20260921

Commits on Sep 4, 2026
- Import the Hopf problem formalization
  Vilin97
  committed
  eb79f1c
- Narrow Hopf problem tactic imports
  Vilin97
  committed
  bc6e898
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  12b4ab2
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  5630fb5
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  bce2a91
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  7069b00
- Credit sources of the six-sphere formalization
  Vilin97
  committed
  401d0fb
- Deduplicate six-sphere coordinates and arguments
  Vilin97
  committed
  b4a4801
Commits on Sep 5, 2026
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  ed74291
Commits on Sep 8, 2026
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  5ed205a
Commits on Sep 10, 2026
Commits on Sep 11, 2026
Commits on Sep 12, 2026
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  251f58e
Commits on Sep 13, 2026
Commits on Sep 14, 2026
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  a3e95db
Commits on Sep 16, 2026
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  2cee31b
Commits on Sep 17, 2026
- Add PentagonalNumberTheoremAnalytic
  
  JonCYeh
  and
  claude
  committed
  38582aa
- Address review: correct two overclaims, narrow imports, fix stale docs
  
  JonCYeh
  and
  claude
  committed
  88d9a56
- Address remaining review findings: dead helper, namespace containment
  
  JonCYeh
  and
  claude
  committed
  393a157
- Satisfy the pool-wide naming linter
  
  JonCYeh
  and
  claude
  committed
  b7ff3fb
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  165d8c7
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  4f1b097
- Address maintainer review: module names, JTP assembly, doc claim
  
  JonCYeh
  and
  claude
  committed
  c336c0f
- Merge branch 'conrad/pentagonal-number-theorem' of https://github.com/JonCYeh/lean-pool into conrad/pentagonal-number-theorem
  Jonathan Conrad
  committed
  576ab60
- Reflow the formal Jacobi scope sentence in the project card
  
  Jonathan Conrad
  and
  claude
  committed
  932556e
- Merge remote-tracking branch 'origin/main' into conrad/pentagonal-number-theorem
  Jonathan Conrad
  committed
  2545129
- Fix entry metadata: qualify Franklin names, add generated project card
  
  Jonathan Conrad
  and
  claude
  committed
  8195b46
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  c3eb0af
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  90ebf06
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  9732c45
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  bcaa4fe
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  c630747
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  f52cda2
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  07807e3
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  6c15871
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  ac4e3c5
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  9ba5071
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  bf84460
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  53eb7aa
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  7b1cba1
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  21c83a5
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  1c30173
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  7f67646
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  f8837dc
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  0570d1b
Commits on Sep 18, 2026
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  0412d84
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  4f28abb
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  9ebe12b
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  bf8261a
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  a7baa0f
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  304301c
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  4f646c0
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  62653ef
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  b66e62a
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  51e54a8
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  59dcaab
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  029a3fe
- Repair the build against Mathlib v4.34.0
  
  Jonathan Conrad
  and
  claude
  committed
  14599b8
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  b367954
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  3692e93
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  9dbde1d
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  806f140
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  0ab4a5e
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  13bce96
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  befcbe5
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  101bdd3
- Port HopfProblem to Mathlib v4.34.0 stable
  
  authored and
  Vilin97 automation
  committed
  fe3c100
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  19e9796
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  3127eb9
Commits on Sep 19, 2026
- feat: import centered maximal-operator bounds
  Vilin97 automation
  committed
  b9d5053
- chore: normalize imported Lean source permissions
  Vilin97 automation
  committed
  d4e0ff5
- docs: align lattice commentary with proved bounds
  Vilin97 automation
  committed
  8ef91db
- style: wrap smearing description
  Vilin97 automation
  committed
  d7d81cd
- feat: import and optimize the complete ACMAX conjecture proof
  Vilin97 automation
  committed
  6198bd2
- perf: bound remaining ACMAX arithmetic contexts
  Vilin97 automation
  committed
  2d02fd7
- style: normalize ACMAX mathematical comment symbols
  Vilin97 automation
  committed
  1c56be3
- style: wrap the degree-log Jensen documentation
  Vilin97 automation
  committed
  7b5e794
- Merge remote-tracking branch 'origin/main' into pr-458
  github-actions[bot]
  committed
  eee4c34
- Merge remote-tracking branch 'origin/main' into pr-455
  github-actions[bot]
  committed
  d030c9e
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  8b56d70
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  70c83b8
- Merge remote-tracking branch 'origin/main' into HEAD
  Vilin97 automation
  committed
  af5fe0b
- refactor: share ACMAX hub-cross leakage estimates
  Vilin97 automation
  committed
  3ed43b5
- Merge remote-tracking branch 'origin/main' into HEAD
  Vilin97 automation
  committed
  053ea98
- fix(ACMax): wrap the completed girth-bound documentation
  Vilin97 automation
  committed
  08d686c
- Merge remote-tracking branch 'origin/main' into pr-458
  github-actions[bot]
  committed
  5b20fbe
- Merge remote-tracking branch 'origin/main' into pr-455
  github-actions[bot]
  committed
  9b0fc33
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  e5fbd7f
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  ddcd945
- Share ACMAX census identities and mirrored path cuts
  Vilin97 automation
  committed
  c1d4f8f
Commits on Sep 20, 2026
- Import Gaussian Moments Conjecture counterexamples
  Vilin97 automation
  committed
  bb17e6d
- Import square-difference-free counterexamples to Naslund conjecture
  Vilin97 automation
  committed
  3cdc9ca
- Separate lift recovery and asymptotic estimates into reusable lemmas
  Vilin97 automation
  committed
  8cd6626
- feat: import Kurosh and sharp Schreier subgroup theorems
  Vilin97 automation
  committed
  4b01fc1
- refactor: reuse Mathlib orbit quotient and internalize Kurosh helpers
  Vilin97 automation
  committed
  8ad293b
- build: record initial DilCat port for reproducible profiling
  Vilin97 automation
  committed
  5d80071
- feat: import dilatations of categories and commutative rings
  Vilin97 automation
  committed
  c137251
- docs: clarify the corrected exponent-profile comparison
  Vilin97 automation
  committed
  59bcd96
- refactor: simplify dilatation uniqueness and preserve base algebra
  Vilin97 automation
  committed
  ba96507
- Merge branch 'main' into conrad/pentagonal-number-theorem
  JonCYeh
  authored
  97a2cb9
- Merge remote-tracking branch 'origin/main' into pr-463
  github-actions[bot]
  committed
  e10a76a
- Merge remote-tracking branch 'origin/main' into pr-462
  github-actions[bot]
  committed
  caeb1e1
- Merge remote-tracking branch 'origin/main' into pr-461
  github-actions[bot]
  committed
  590aeb8
- Merge remote-tracking branch 'origin/main' into pr-460
  github-actions[bot]
  committed
  fb8c29e
- Merge remote-tracking branch 'origin/main' into pr-458
  github-actions[bot]
  committed
  c6d70b8
- Merge remote-tracking branch 'origin/main' into pr-455
  github-actions[bot]
  committed
  653cd75
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  644e0ef
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  ff7df9b
- refactor: share Kurosh product and edge equivalences
  Vilin97 automation
  committed
  2fe8fe6
- refactor: share localization faithfulness proofs
  Vilin97 automation
  committed
  c5c52fd
Commits on Sep 21, 2026
- Merge remote-tracking branch 'origin/main' into pr-463
  github-actions[bot]
  committed
  0bd80b4
- Merge remote-tracking branch 'origin/main' into pr-462
  github-actions[bot]
  committed
  946a309
- Merge remote-tracking branch 'origin/main' into pr-461
  github-actions[bot]
  committed
  497c75e
- Merge remote-tracking branch 'origin/main' into pr-460
  github-actions[bot]
  committed
  9575376
- Merge remote-tracking branch 'origin/main' into pr-458
  github-actions[bot]
  committed
  aace611
- Merge remote-tracking branch 'origin/main' into pr-455
  github-actions[bot]
  committed
  147c048
- Merge remote-tracking branch 'origin/main' into pr-446
  github-actions[bot]
  committed
  5b846a0
- Merge remote-tracking branch 'origin/main' into pr-392
  github-actions[bot]
  committed
  92f28f2
- Merge current main before final PR validation
  Vilin97
  committed
  658cee4
- Merge remote-tracking branch 'origin/main' into HEAD
  Vilin97
  committed
  6251f09
- Clarify the topological six-sphere identification
  Vilin97
  committed
  4c678f0
- Merge reviewed PR #461 into integration batch
  Vilin97
  committed
  c33c463
- Merge reviewed PR #462 into integration batch
  Vilin97
  committed
  5aec104
- Merge reviewed PR #463 into integration batch
  Vilin97
  committed
  c41f308
- Merge reviewed PR #460 into integration batch
  Vilin97
  committed
  aabdd2a
- Merge reviewed PR #455 into integration batch
  Vilin97
  committed
  42a854e
- Merge reviewed PR #446 into integration batch
  Vilin97
  committed
  953cda5
- Merge reviewed PR #458 into integration batch
  Vilin97
  committed
  1a5b29c
- Merge reviewed PR #392 into integration batch
  Vilin97
  committed
  e3534f0

Commits

Commits on Sep 4, 2026

Commits on Sep 5, 2026

Commits on Sep 8, 2026

Commits on Sep 10, 2026

Commits on Sep 11, 2026

Commits on Sep 12, 2026

Commits on Sep 13, 2026

Commits on Sep 14, 2026

Commits on Sep 16, 2026

Commits on Sep 17, 2026

Commits on Sep 18, 2026

Commits on Sep 19, 2026

Commits on Sep 20, 2026

Commits on Sep 21, 2026