jdb1729
Joined 8 years ago
Karma
218
Submissions
31
Member since
Sep 25
Recent submissions
Comment · 10 days ago
Comment · 10 days ago
> The new result does not directly imply new complexity bounds for polynomial multiplication over a fixed finite field, say multiplication in F2[x]. The state of the art for this problem is an algorithm that multiplies polynomials of degree n in time O(n log n 4^log*(n)) [HvdH19].
@platypii and I obtained a Lean proof of the same improvement for DFT over prime-order finite fields (yielding polynomial multiplication via the convolution theorem): https://github.com/platypii/integer-mult-bounds-lean/blob/ma...
Comment · 10 days ago
For one thing, the RAM model isn't fine-grained equivalent to MTTM (an example is https://en.wikipedia.org/wiki/Counting_sort which is linear-time on RAM but not MTTM). So, the result might not be the same. But also, Mathlib lacks a RAM machine implementation. So any proof would rest on a custom definition stack which would make it difficult to audit.
Comment · 10 days ago
The integer multiplication improvements generalize to DFT over prime-order finite fields, see: https://github.com/platypii/integer-mult-bounds-lean/blob/ma...
Comment · 10 days ago
@platypii and I have been pursuing Lean verification of improvements to kappa here: https://github.com/platypii/integer-mult-bounds-lean
Current status of the campaign: kappa >= 2^-14.38 proved unconditionally on Mathlib's TM2 machine. Contributions welcome!
Comment · 22 days ago
This is a Lean-verified variation of the OpenAI proof for pi.
Comment · 22 days ago
I don't know, what if someone made an app or a website where you get a dollar for every bit until an odd prime hits. The theorem says how much to price each spin to guarantee a long-term profit for the house (somewhere between tree fiddy and half a quadrillion dollars).
Actually, nothing practical, just sharing my love of math and excitement about the new possibilities of formal verification being unlocked.
Comment · 22 days ago
Well, not really, the contrapositive is that if the series diverges the Riemann Hypothesis would be refuted. But few doubt that the Riemann Hypothesis is true. So using it as an assumption merely makes the convergence slightly iffy. For another example of its use, see the deterministic Miller primality test: https://en.wikipedia.org/wiki/Miller–Rabin_primality_test
Comment · 22 days ago
A nom de OOM.
Comment · 25 days ago
To be forthright it wasn't me doing most of the thinking! I'm taking my time to understand it. The issue with the bases as I understand it is that we need log(b) < 1 for convergence which only works for b = 2 < e. Check out the other math.SE answer which explains the heuristic but reaches the wrong conclusion by being off by a factor of 2.
Comment · 26 days ago
Yes, see the table in Remark 7.3 on page 5, it exceeds 3.5, with growth slowing to a crawl. But the calculations mean little, sum(1/p) grows as divergent log(log(n)), so it also has the appearance of convergence on that basis. Many on math.SE argued for divergence (answers since deleted)! Although the proved upper bound is 5e14, heuristically it should be less than 4. I doubt RH is truly necessary. But even relying on RH, the exact value of the sum is elusive.
Comment · 27 days ago
The reciprocal sum of the prime-prefix-free numbers (https://oeis.org/A287117) converges to a number less than 5*10^14, conditional on the Riemann Hypothesis.
This Lean-verified proof answers a question I posed 10 years ago: https://math.stackexchange.com/questions/2288648/does-the-su...
An equivalent version: if we start with 1 and then output a stream of random bits, reading the number as a big-endian binary number at each step (so each time a bit arrives, the number is multiplied by 2 and 1 is either added or not), the expected time until the number is an odd prime is finite.
The result is fully formalized in Lean by @platypii and myself (on Mathlib's TM2 machine), with ongoing improvements to the exponent (currently at 1-2^-14.38): https://github.com/platypii/integer-mult-bounds-lean
Contributions are welcome!