Issues

• Propose project: coboundary-k3-lean (the Sym(3) coboundary constant of K_k is k/3 for 4 ≤ k ≤ 8, both bounds in Lean)

  LeanPool/lean-pool#725 · Filter by author dicipler-pixel opened on Oct 29, 2026

• Noisy proofs relying on loopholes in flexible-tactic linter

  LeanPool/lean-pool#724 · Filter by author loefflerd opened on Oct 28, 2026
  2

• Long proofs exploiting loopholes in proof-length checker

  LeanPool/lean-pool#723 · Filter by author loefflerd opened on Oct 28, 2026

• Proposal: lean-ramsey (finite Ramsey theory on SimpleGraph.EdgeLabeling)

  LeanPool/lean-pool#721 · Filter by author Egly443 opened on Oct 27, 2026

• Repository proposal: Ginibre Poincaré inequalities and full-paper formalization

  LeanPool/lean-pool#644 · Filter by author djalilchafai opened on Oct 12, 2026

• Add support for formalization.yaml

  LeanPool/lean-pool#466 · Filter by author Vilin97 opened on Sep 20, 2026

• Track and reuse version bumps of imported projects

  LeanPool/lean-pool#346 · Filter by author Vilin97 opened on Aug 23, 2026