All pull requests

Pull requests

• Free runner disk before every pool-build restore and lint for it

  #764·Vilin97 opened Nov 6, 2026Collaborator·

  ·
  8

• Optimize PLAcceleratedNesterovLean arithmetic proofs and imports

  #763·Vilin97 opened Nov 6, 2026Collaborator·

  ·
  3

• Import the Goldberg–Seymour edge-coloring theorem

  #761·Vilin97 opened Nov 5, 2026Collaborator·

  ·
  18

• ci(proof-profile): free runner disk before restoring caches

  needs-maintainer
  #760·Vilin97 opened Nov 5, 2026Collaborator·

  ·
  3

• Refresh README stats and NOTICE daily from the docs workflow

  needs-maintainer
  #758·Vilin97 opened Nov 5, 2026Collaborator·

  ·
  3

• Make every Lean warning a compile error (warningAsError, like Tau Ceti)

  #751·Vilin97 opened Nov 5, 2026Collaborator·2 of 3 tasks·

  ·
  5

• Optimize InfiniteConnesRigidity proof elaboration

  #749·Vilin97 opened Nov 4, 2026Collaborator·

  ·
  2

• Import explicit planar distinct-distance improvement to 43n/120

  needs-maintainer
  #746·Vilin97 opened Nov 4, 2026Collaborator·

  ·
  13

• Optimize MetricCodes algebra proofs and elaboration

  #743·Vilin97 opened Nov 4, 2026Collaborator·

  ·
  3

• perf(QuantumQuery): share spectral estimates and narrow proof inputs

  #742·Vilin97 opened Nov 4, 2026Collaborator·

  ·
  3

• Optimize QuantumParallelRepetition matrix and history proofs

  #734·Vilin97 opened Nov 3, 2026Collaborator·

  ·
  1

• Reduce SmallUndecidableGroups compilation memory

  #714·Vilin97 opened Oct 23, 2026Collaborator·

  ·
  3

• perf(Incompleteness): avoid kernel reduction in term construction proofs

  #713·Vilin97 opened Oct 23, 2026Collaborator·

  ·
  3

• Optimize PhaseRetrieval analytic proofs and shared estimates

  #701·Vilin97 opened Oct 21, 2026Collaborator·

  ·
  4

• perf: reduce Ehrhart volume proof elaboration

  #697·Vilin97 opened Oct 20, 2026Collaborator·

  ·
  3

• perf(PDL): shorten tableau compilation dependencies

  #682·Vilin97 opened Oct 19, 2026Collaborator·

  ·
  4

• Optimize NonSoficGroup proof elaboration and private imports

  #679·Vilin97 opened Oct 18, 2026Collaborator·

  ·
  2

• Import anisotropic and classical Carleson formalization

  #666·Vilin97 opened Oct 17, 2026Collaborator·

  ·
  13

• Retire public version-bump jobs in favor of private VM automation

  #660·Vilin97 opened Oct 16, 2026Collaborator·

  ·
  3

• Import Parikh's theorem and certified semilinear grammar compiler

  #653·Vilin97 opened Oct 14, 2026Collaborator·

  ·
  11

• WIP: Add finite-dimensional copulas and Sklar's theorem

  #639·Vilin97 opened Oct 11, 2026Collaborator·

  ·
  4

• WIP: Remove blanket section exposure across Lean Pool

  needs-manual-rebase
  #529·Vilin97 opened Sep 25, 2026Collaborator·

  ·
  11

• WIP: Import Riemannian curvature and geometric analysis toward Ricci flow

  #512·Vilin97 opened Sep 21, 2026Collaborator·

  ·
  26

• WIP: Import Coarse-graining theory for elliptic equations

  #507·Vilin97 opened Sep 21, 2026Collaborator·

  ·
  29

• WIP: Import Local and global class field theory

  #506·Vilin97 opened Sep 21, 2026Collaborator·

  ·
  24