Repository navigation

merge upstream - #2

Merged

alreadydone merged 37 commits into

alreadydone:Mostow_rigidity+from

leanprover:main

Aug 1, 2026

Commits on Jul 22, 2026
- fix: require [T2Space M] in morse_inequality and weak_morse_inequality (#480)
  
  kim-em
  and
  claude
  authored
  37a88ab
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  a5ae891
Commits on Jul 26, 2026
- Add derived solidification of free CW complexes challenge (light condensed mathematics) (#471)
  
  dagurtomas
  and
  claude
  authored
  2174eb0
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  2a12548
Commits on Jul 29, 2026
- chore: bump toolchain to v4.32.2
  kim-em
  committed
  283d374
- fix(generate): skip leading copyright block in import prelude (#467)
  
  authored
  90175b9
- feat(RepresentationTheory): add Ado theorem problems (#483)
  kim-em
  authored
  4ab80fc
- Merge pull request #484 from leanprover/chore/bump-toolchain-v4.32.2
  kim-em
  authored
  e5eb313
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  074f4d5
Commits on Jul 30, 2026
Commits on Jul 31, 2026
- feat: add Avila-Jitomirskaya Ten Martini eval problem (#495)
  kim-em
  authored
  ccf5d18
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  d3729fd
- ci: update action runtimes and Go toolchain (#496)
  kim-em
  authored
  cf5b60d
- feat: add Huh strong Mason eval problem (#491)
  kim-em
  authored
  01536fb
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  6390c4e
- feat: add Duminil-Copin honeycomb connective-constant eval problem (#492)
  kim-em
  authored
  45d79e3
- feat: add Maynard Duffin-Schaeffer eval problem (#493)
  kim-em
  authored
  837e730
- ci: use GitHub App client ID (#498)
  kim-em
  authored
  a969c76
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  344d00f
- feat: add Fourier interpolation in dimensions 8 and 24 (#494)
  kim-em
  authored
  2dc91d1
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  3f3786f
Commits on Aug 1, 2026
- docs: align Rokhlin description with formal target (#501)
  kim-em
  authored
  20c7831
- docs: clarify Riesz brothers formal target (#502)
  kim-em
  authored
  0d44a77
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  d1ab347
- chore: regenerate generated/ workspaces
  lean-eval-regenerator[bot]
  committed
  2d02061

Commits

Commits on Jul 22, 2026

Commits on Jul 26, 2026

Commits on Jul 29, 2026

Commits on Jul 30, 2026

Commits on Jul 31, 2026

Commits on Aug 1, 2026