Zulip Chat Archive
Stream: PrimeNumberTheorem+
Topics:
- Upstreaming (9 messages, latest: Dec 19 2025 at 04:25)
- Explicit estimates: \(M(x)\), \(\psi(x)\) (18 messages, latest: Dec 18 2025 at 04:53)
- mathlib bump (138 messages, latest: Dec 15 2025 at 16:56)
- How to make formalizing limits less tedious? (10 messages, latest: Nov 27 2025 at 23:31)
- 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)
- Wiener-Ikehara source (99 messages, latest: Jul 06 2025 at 03:27)
- 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)
- What route to take to Chebotarev? (1 message, latest: Feb 01 2025 at 23:40)
- 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: Dec 20 2025 at 21:32 UTC