All pull requests

Pull requests

• Solution: Ville inequality for testing by betting

  #566·deadczarvc opened Oct 1, 2026Contributor·

  ·
  2

• quality: read an axiom list that Lean wrapped over several lines

  #564·deadczarvc opened Oct 1, 2026Contributor·

  ·
  5

• WIP: Use module system in Lean tooling scripts

  #561·Vilin97 opened Oct 1, 2026Owner·4 of 5 tasks·

  ·

• Import Sendov's conjecture and the Phelps–Rodriguez conjecture

  #556·Vilin97 opened Oct 1, 2026Owner·

  ·
  9

• Import viscosity solution theory and Aleksandrov differentiability

  #553·Vilin97 opened Sep 30, 2026Owner·

  ·
  8

• Import order-closure and weak Fatou formalization

  #536·Vilin97 opened Sep 26, 2026Owner·

  ·
  13

• WIP: Remove blanket section exposure across Lean Pool

  #529·Vilin97 opened Sep 25, 2026Owner·

  ·
  7

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

  #512·Vilin97 opened Sep 21, 2026Owner·

  ·
  23

• WIP: Import Davis–Kahan rotation of eigenvectors

  #511·Vilin97 opened Sep 21, 2026Owner·

  ·
  25

• Import Brill–Noether theory and gonality of finite graphs

  #510·Vilin97 opened Sep 21, 2026Owner·

  ·
  24

• WIP: Import Equal-area and equal-perimeter convex partitions

  #508·Vilin97 opened Sep 21, 2026Owner·

  ·
  23

• WIP: Import Coarse-graining theory for elliptic equations

  #507·Vilin97 opened Sep 21, 2026Owner·

  ·
  15

• WIP: Import Local and global class field theory

  #506·Vilin97 opened Sep 21, 2026Owner·

  ·
  19

• Import Stafford’s Conjecture 3.8 formalization

  #503·Vilin97 opened Sep 21, 2026Owner·

  ·
  33

• WIP: import Markoff mod p

  #502·Vilin97 opened Sep 21, 2026Owner·

  ·
  18

• WIP: Import Beyond Bethe permanent approximation

  #500·Vilin97 opened Sep 21, 2026Owner·

  ·
  17

• WIP: import the Regts–Sevenster conjecture formalization

  #499·Vilin97 opened Sep 21, 2026Owner·

  ·
  27

• Import endpoint estimates for Stein's purely quadratic Carleson operator

  #498·Vilin97 opened Sep 21, 2026Owner·

  ·
  19

• Import Parameter-Free Gradient Minimization in l_p Geometry

  #497·Vilin97 opened Sep 21, 2026Owner·

  ·
  19

• Import Nash's smooth isometric embedding theorem

  #496·Vilin97 opened Sep 21, 2026Owner·

  ·
  18

• Import complete unitary dilation and Crouzeix–Palencia development

  #485·Vilin97 opened Sep 21, 2026Owner·

  ·
  30