https://eprint.iacr.org/2022/439

this doesn't use the literal n \log n algorithm, which may be galactic. but it uses fundamentally similar techniques.

1. if this is true, it is interesting, and

2. the exposition of this is a huge pile of slop.

This requires mathematicians to have to clean up the slop for it to be useful. It has happened for most LLM-generated proofs in the last few months. Anthropic explicitly payed two top complexity theorists to do it for the 3SUM and APSP breakthrough.

They didn't do this because those complexity theorists are advocating for a tyranny of the illiterate lmao

https://en.wikipedia.org/wiki/%C3%89l%C3%A9ments_de_math%C3%...

It has many benefits, and many people appreciate the books. It also has many downsides. For example, they started publishing in 1939. As part of this, they needed to work through the basis that most other mathematical objects are defined in terms of (they used sets).

Unfortunately for them, contemporaneously with their work, other mathematicians were beginning to define mathematical objects (categories) that can be an alternative basis for mathematics, which many modern expositions prefer to sets. So, their approach either

1. needed a massive "refactoring", or

2. would be hopelessly dated.

They ended up going with the approach that is now dated. It may sound peculiar that mathematics can be "dated". But it very much can. The mathematics community can go through many different styles for how to explain/collect mathematical understanding. Different styles can have different benefits, and be easier/harder for different subfields. A simplified/unified perspective will necessarily privilege certain perspectives.

It is analogous to how you might want there to be a simplified/unified (set of) libraries for programming. Perhaps that everyone uses. This sounds nice, and many programming languages do this with their standard libraries. But these always make concessions! I'll speak about Rust's, as I'm most familiar

1. fallible allocation or infallible allocation?

2. C-style strings or (ptr, len) strings?

3. Should interfaces take as input &mut [T] references, or should they take as input T in an "owned" way (this would make compatibility with io_uring easier)

for each, it is not that one answer is right. Both can be argued for. You have to choose one. The one choice may not be satisfactory for every practitioner though.

Now, there are some critiques you can have of this. Namely, it is possible that these novel algorithms have significant trade-offs that make them almost never worthwhile in practice. "Fast" matrix multiplication algorithms are typically of this form. So perhaps this all points towards a deficiency in big O notation, which can be deceptive. But, for people who care about optimizing asymptotic complexity, it is still interesting.

Non-deterministic can be explained in several ways. One is in terms of a hypothetical "nondeterministic Turing machine" with certain non-physically realizable properties. The easier way is that a NP problem gets as input not only the problem instance x, but a "witness" w, that may depend on the problem instance. This witness generally makes the problem of deciding the problem instance straightforward (e.g. for SAT, x is the SAT instance, and w is a description of how to set the variables so that it is true).

1. examine A, and

2. examine C, and

3. rely on the Lean kernel to ensure that all of the interior transitions are correct.

Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).

I would imagine many people would find support of a modern-day, somewhat influential (he has several followers in Trump's administration, as well as among several right-wing billionaires) monarchist to be notable/distasteful.

https://en.wikipedia.org/wiki/57_(number)

https://pmc.ncbi.nlm.nih.gov/articles/PMC5230747/

roughly, it reviews common techniques in neuroscience, and comes to the conclusion that they would not be able to understand even simple computing platforms that we have perfect information for (and can perfectly stimulate any internal connection, can perfectly read out the values on any internal connection, etc).

As a trivial example, in lean you can work with probability theory/measure theory. This has oodles of non-constructive parts, but we can ignore that for now. As part of this, you can use the probabilistic method. For example, if you want to prove that codes with optimal parameters exist, for many noise models it is known that sampling a code randomly from an appropriate (and often naive) distribution will yield a code with optimal parameters.

You should be able to prove this in lean (or any other theorem prover). But you cannot construct these codes. While you can sample a code randomly, verifying a code has good parameters is typically NP-hard (e.g. it is an instance of the minimum distance problem). So, you cannot (efficiently) "construct" a good code in lean4, despite being able to prove one exists.

This seems analogous to me that you could validate that a non-constructive proof is correct in lean4. Sure, it would be nice if the proof was constructive. But it isn't, and encoding it into a computer shouldn't give you that (non-trivial) property for free.