Skip to content

Import polylean formalization #109

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 8 commits into from
May 19, 2026
Merged

Import polylean formalization #109

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
203dfb6
Vendor Polylean unit conjecture infrastructure
Vilin97 May 18, 2026
c7304a8
Restore polylean Gardam theorem
Vilin97 May 19, 2026
05759bb
Replace Gardam native decide proofs
Vilin97 May 19, 2026
f65b963
Add Polylean graph paths
Vilin97 May 19, 2026
7ce8ee5
Add remaining Polylean importable modules
Vilin97 May 19, 2026
b1185ec
Clean Polylean build warnings
Vilin97 May 19, 2026
2185bf3
Merge remote-tracking branch 'origin/main' into import/polylean-retry…
Vilin97 May 19, 2026
547524c
Merge remote-tracking branch 'origin/main' into tmp/109
Vilin97 May 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 22 additions & 0 deletions LeanPool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -336,6 +336,28 @@ import LeanPool.PolyaEnumerationTheorem.Concrete
import LeanPool.PolyaEnumerationTheorem.PermutationAuxiliary
import LeanPool.PolyaEnumerationTheorem.ReductionToFin
import LeanPool.PolyaEnumerationTheorem.StirlingFirstKindSum
import LeanPool.Polylean
import LeanPool.Polylean.Complexes.GraphPaths
import LeanPool.Polylean.Complexes.Structures.Category
import LeanPool.Polylean.Complexes.Structures.Groupoid
import LeanPool.Polylean.Complexes.Structures.Quiver
import LeanPool.Polylean.ConjInvLength.Length
import LeanPool.Polylean.ConjInvLength.LengthBound
import LeanPool.Polylean.ConjInvLength.MemoLength
import LeanPool.Polylean.ConjInvLength.ProvedBound
import LeanPool.Polylean.ConjInvLength.WordTree
import LeanPool.Polylean.UnitConjecture
import LeanPool.Polylean.UnitConjecture.AddFreeGroup
import LeanPool.Polylean.UnitConjecture.Cocycle
import LeanPool.Polylean.UnitConjecture.EnumDecide
import LeanPool.Polylean.UnitConjecture.FreeModule
import LeanPool.Polylean.UnitConjecture.GardamGroup
import LeanPool.Polylean.UnitConjecture.GardamTheorem
import LeanPool.Polylean.UnitConjecture.GroupRing
import LeanPool.Polylean.UnitConjecture.MetabelianGroup
import LeanPool.Polylean.UnitConjecture.Tactics
import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets
import LeanPool.Polylean.UnitConjecture.TorsionFree
import LeanPool.RamanujanTauMissesPrimes
import LeanPool.RamanujanTauMissesPrimes.Solution
import LeanPool.RiemannMappingTheorem
Expand Down
27 changes: 27 additions & 0 deletions LeanPool/Polylean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
/-
Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Siddhartha Gadgil, Anand Rao
-/

import LeanPool.Polylean.UnitConjecture
import LeanPool.Polylean.Complexes.GraphPaths
import LeanPool.Polylean.Complexes.Structures.Category
import LeanPool.Polylean.Complexes.Structures.Groupoid
import LeanPool.Polylean.Complexes.Structures.Quiver
import LeanPool.Polylean.ConjInvLength.Length
import LeanPool.Polylean.ConjInvLength.LengthBound
import LeanPool.Polylean.ConjInvLength.MemoLength
import LeanPool.Polylean.ConjInvLength.ProvedBound
import LeanPool.Polylean.ConjInvLength.WordTree

/-!
# Polylean Unit Conjecture Counterexample

Source: url:https://github.com/siddhartha-gadgil/Polylean
Authors: Siddhartha Gadgil, Anand Rao
Status: verified
Main declarations: `LeanPool.Polylean.P.torsionFree`, `LeanPool.Polylean.Gardam.GardamTheorem`
Tags: algebra, group-theory, ring-theory, unit-conjecture
MSC: 16S34, 20F65
-/
Loading
Loading