jdb1729

> It would be good to have a formalised proof of the o(n log n) result, for example in Lean. As far as I can tell, one does not yet exist.

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!

> 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...

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.

The integer multiplication improvements generalize to DFT over prime-order finite fields, see: https://github.com/platypii/integer-mult-bounds-lean/blob/ma...

@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!

This is a Lean-verified variation of the OpenAI proof for pi.

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.

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

A nom de OOM.

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.

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.

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.

Here it is proved that for all epsilon > 0 and sufficiently large n there exists a Carmichael number in the interval (n, n^(1+epsilon)] and furthermore it can be found along with its full factorization in time exp(O(log(log(n)) * log(log(log(n)))) on Mathlib's multi-stack Turing machine model. Formally verified in Lean.

Ita, feedbackum acceptum! Thanks for taking the tempum to check it out, also to whomever gave the astra!

One way I felt the prerogative to influence it was in choice of vocabulary, for example "files" are plicae, non fasciculi, brevity FTW. I have a (private) CLAUDIUS.md file where I accumulated such guidance. Frankly I can't really tell where it lies on the spectrum of classical to vulgar, my memories of reading Cicero and Pliny have faded quite a bit, but I understand your point about the barbaric word order (next expeditio I'll take this into account). But it was still a worthwhile campaign in terms of refreshing that knowledge. Salve!

Sic itur ad astra! I spent some time and tokens generating these C99 applications and libraries all in classical Latin: https://github.com/jdb19937/apotheca. They all build with this C99 compiler + arm64 assembler + linker toolchain https://github.com/jdb19937/ccc (CCC = 300) which is included. But my favorite one of these repo is the 100+ test cases https://github.com/jdb19937/corpus that I used to iterate the compiler to bootstrappability. Nota: README.md ignorandum est. Anglice scriptum est ad barbaros ineruditos pecunia emungendos, lege LEGEME.md.

Four dozen + 1 = 7^2 years ago, our fathers received a signal...

I assume that too.

But I might be over median!

Here is an argument I made that it is NP-complete to determine if a number n is the product of two numbers that differ by less than the fourth root of n:

https://cstheory.stackexchange.com/a/37439

5.5 bits is also the average information content of a single run of the GHZ experiment. In this setup three parties independently choose a binary detector setting and each observe a binary outcome. The first two parties observe an independent random bit regardless of their settings. If an odd number of the parties have their setting "on", then the third party also observes an independently random bit (6 bits total to record, 3 for the settings and 3 for the observations). But if an even number of of the three settings are "on", then the third party's observation is completely determined by the other 5 bits. When the settings are chosen randomly these two possibilities are equally likely so on average it takes 5.5 bits to record the results of the experiment.

Yes, you can zoom in the map to see the generated details.

I've been building this site over the last year. An autoencoder reduces user-submitted images ("peaple") down to 3KB and reconstructs them at 128x128 using pixel loss, then they are sent through a series of GAN-trained upscaling enhancers to generate pics at higher resolutions.

On the site you can browse existing peaple, upload new peaple, generate new ones from random input, blend peaple with each other, explore their infinite virtual family trees, and apply styling effects.

Excited to hear your feedback!