Zulip Chat Archive

Stream: PrimeNumberTheorem+

Topics:

IwaniecKowalski (24 messages, latest: Feb 25 2026 at 16:07)
How I use Aristotle (4 messages, latest: Feb 24 2026 at 00:28)
Personal log (14 messages, latest: Feb 23 2026 at 05:06)
Fixing a sign error in Erdos 392 (6 messages, latest: Feb 23 2026 at 01:07)
New subproject: Ramanujan's inequality (5 messages, latest: Feb 19 2026 at 01:00)
LeanCert imported (8 messages, latest: Feb 18 2026 at 23:20)
Let us formalize an appendix (70 messages, latest: Feb 18 2026 at 17:30)
Log tables (16 messages, latest: Feb 18 2026 at 02:14)
New subproject: Odd goldbach for small n (22 messages, latest: Feb 17 2026 at 21:50)
New miniproject: Chebyshev bounds (8 messages, latest: Feb 17 2026 at 21:09)
LeanCert for numerical log bounds (re: PNT#892, PNT#914) (73 messages, latest: Feb 16 2026 at 22:16)
New subproject: CH2 (16 messages, latest: Feb 15 2026 at 21:10)
New miniproject: Primes in short intervals (9 messages, latest: Feb 13 2026 at 11:33)
Starting on FKS2 (39 messages, latest: Feb 13 2026 at 05:54)
Starting on BKLNW (87 messages, latest: Feb 10 2026 at 06:49)
CI issues (78 messages, latest: Feb 09 2026 at 19:26)
Bounds on LCM(1..n) in Mathlib (4 messages, latest: Feb 06 2026 at 16:29)
Formalizing Riemann-Stieltjes theory (56 messages, latest: Feb 04 2026 at 03:24)
Strong PNT (2 messages, latest: Feb 02 2026 at 14:29)
norm_add₄_le (16 messages, latest: Jan 31 2026 at 18:32)
Miniproject: prove that li(x)=Li(x)+li(2) and li(2)~ 1.0451 (31 messages, latest: Jan 28 2026 at 22:48)
Let us formalize a lemma (19 messages, latest: Jan 28 2026 at 20:19)
Riemann integrability (3 messages, latest: Jan 27 2026 at 22:50)
Explicit estimates, outstanding tasks v2. (213 messages, latest: Jan 25 2026 at 12:44)
Fejér's theorem has just been formalized (6 messages, latest: Jan 23 2026 at 18:01)
Appendix A of BKLNW (1 message, latest: Jan 23 2026 at 05:21)
Code/annotation standards and maintainability (2 messages, latest: Jan 22 2026 at 04:58)
Prime number theorem in AP (8 messages, latest: Jan 22 2026 at 00:46)
A quick subproject: Costa Pereira inequality (11 messages, latest: Jan 21 2026 at 19:20)
Formalizing Wheeden-Zygmund via Aristotle (6 messages, latest: Jan 21 2026 at 18:28)
Experimental refactoring of LCM.lean (1 message, latest: Jan 21 2026 at 00:11)
Fourier decay, and what it confirms about real-analysis gaps (44 messages, latest: Jan 20 2026 at 13:12)
mobius lemma 2 (9 messages, latest: Jan 19 2026 at 00:11)
Diophantine approximation (or: a formalization surprise) (8 messages, latest: Jan 18 2026 at 17:22)
Duality principle (28 messages, latest: Jan 18 2026 at 01:34)
TME-EMT (3 messages, latest: Jan 17 2026 at 21:17)
Do we really need Stieltjes integral? (5 messages, latest: Jan 17 2026 at 09:47)
Hadamard factorization - PR ideas (3 messages, latest: Jan 16 2026 at 20:17)
Disclosure of AI tools in PRs (7 messages, latest: Jan 16 2026 at 19:25)
mathlib bump (145 messages, latest: Jan 15 2026 at 22:25)
Some Rosser-Schoenfeld identities (6 messages, latest: Jan 15 2026 at 17:01)
Update on Consequences (3 messages, latest: Jan 15 2026 at 03:38)
Update on tertiary estimate projects (75 messages, latest: Jan 15 2026 at 01:08)
Euler-Maclaurin, Poisson summation (22 messages, latest: Jan 13 2026 at 13:55)
What route to take to Chebotarev? (2 messages, latest: Jan 12 2026 at 23:32)
Project Dashboard (4 messages, latest: Jan 12 2026 at 18:56)
How to extract the blueprint tex files locally? (85 messages, latest: Jan 12 2026 at 15:33)
Wiener-Ikehara source (100 messages, latest: Jan 12 2026 at 12:35)
A small cautionary tale with autoformalization (1 message, latest: Jan 10 2026 at 20:20)
Blueprint not compiling in repo despite passing CI (13 messages, latest: Jan 09 2026 at 03:15)
Math-Inc Pulls (18 messages, latest: Jan 08 2026 at 20:11)
Gamma Incomplete Remarks (1 message, latest: Jan 08 2026 at 07:26)
Aristotle as solver for mu_pnt and mu_pnt_alt (19 messages, latest: Jan 05 2026 at 23:05)
LeanCopilot and other imports (3 messages, latest: Jan 04 2026 at 21:32)
Explicit estimates: \(M(x)\), \(\psi(x)\) (21 messages, latest: Jan 04 2026 at 19:24)
N(T) (7 messages, latest: Jan 04 2026 at 09:16)
How to make formalizing limits less tedious? (11 messages, latest: Jan 03 2026 at 12:20)
Upstreaming (10 messages, latest: Dec 27 2025 at 09:25)
Contradictory implicit assumptions in auto_cheby (12 messages, latest: Nov 21 2025 at 01:45)
Formalizing Selberg Sieve Weights & Errors in Lean 4 (33 messages, latest: Oct 15 2025 at 18:45)
Merging with Morph (34 messages, latest: Oct 14 2025 at 00:04)
Tidying ZetaBounds (2 messages, latest: Aug 18 2025 at 14:23)
Toolchain help (4 messages, latest: Aug 14 2025 at 21:16)
MediumPNT is Done! (8 messages, latest: Jul 29 2025 at 17:24)
Formalizing Mertens-type Lower Bounds for Möbius/Euler Totie (5 messages, latest: Jul 27 2025 at 21:49)
Upstreaming to Mathlib (10 messages, latest: Jul 25 2025 at 15:19)
Things to work on (2 messages, latest: Jul 06 2025 at 03:23)
Outstanding Tasks V7 (14 messages, latest: May 05 2025 at 13:31)
Sieve from mathlib (3 messages, latest: Apr 02 2025 at 16:10)
PNT+ used to prove irrationality of zeta(3) (7 messages, latest: Mar 26 2025 at 02:47)
MathOverflow question (1 message, latest: Mar 02 2025 at 20:44)
Outstanding Tasks V6 (72 messages, latest: Feb 18 2025 at 22:14)
Update (10 messages, latest: Feb 17 2025 at 11:15)
Orthogonality of Dirichlet characters (1 message, latest: Nov 05 2024 at 15:32)
Is anyone proving the pi_alt theorem (3 messages, latest: Oct 25 2024 at 15:24)
restarting progress (60 messages, latest: Oct 20 2024 at 17:27)
Classical error term in Isabelle! (1 message, latest: May 08 2024 at 16:05)
Fourier analysis (1 message, latest: Apr 17 2024 at 12:52)
Connecting with EulerProducts/PNT.lean (51 messages, latest: Apr 08 2024 at 20:31)
Outstanding Tasks, V5 (85 messages, latest: Apr 08 2024 at 20:12)
Outstanding Tasks, V4 (80 messages, latest: Apr 04 2024 at 17:17)
#11776 higher derivative of Fourier transform (3 messages, latest: Mar 30 2024 at 03:06)
Potentially useful results (18 messages, latest: Mar 07 2024 at 15:49)
LSeries.term (7 messages, latest: Mar 06 2024 at 14:10)
Outstanding Tasks, V3 (23 messages, latest: Mar 05 2024 at 22:43)
Fourier inversion (5 messages, latest: Feb 23 2024 at 07:43)
Outstanding Tasks, V2 (120 messages, latest: Feb 22 2024 at 09:45)
L-series (26 messages, latest: Feb 20 2024 at 18:40)
Blueprint colors (54 messages, latest: Feb 15 2024 at 15:21)
PR related to big O notation (2 messages, latest: Feb 14 2024 at 14:35)
Uh Oh, build failed (18 messages, latest: Feb 07 2024 at 22:04)
On embedding blueprint TeX within Lean (3 messages, latest: Feb 07 2024 at 19:40)
Weierstrass M-test (15 messages, latest: Feb 06 2024 at 01:00)
Outstanding Tasks, V1 (33 messages, latest: Feb 05 2024 at 06:54)
Beginner Lean Question (24 messages, latest: Feb 04 2024 at 23:23)
caching issue (2 messages, latest: Feb 03 2024 at 04:54)
No longer compiling (5 messages, latest: Feb 02 2024 at 22:46)
Brun-Titchmarsh type theorem for Theorem 12 (5 messages, latest: Feb 02 2024 at 02:03)
Decision to be made on (2 \pi i) factors (3 messages, latest: Feb 01 2024 at 16:05)
Smooth Urysohn Lemma (16 messages, latest: Feb 01 2024 at 02:24)
How to spell asymptotics? (8 messages, latest: Jan 31 2024 at 16:34)
Broken link in blueprint (8 messages, latest: Jan 31 2024 at 04:38)
lean_exe build target? (3 messages, latest: Jan 31 2024 at 00:15)
Shorthand project name (9 messages, latest: Jan 30 2024 at 16:06)
stream events (1 message, latest: Jan 30 2024 at 12:42)

Last updated: Feb 28 2026 at 14:05 UTC