stabbles

That's the theme of this reflection: https://proofsandprompts.com/2026/10/08/why-i-chose-to-do-ma...

> In our view, these manuscripts are best understood as a form of raw research data. To convert this raw research data into scientific understanding, in this release we are experimenting with a new approach

Mathematics and computer science are turning into an empirical science

See https://www.swisstopo.admin.ch/en/height-model-swissalti3d, which is an excellent resource.

Hot patching is itself a liability

"How to rewrite all software in Rust"

I'm reading this paragraph with the precedent of AlphaGo in mind, where none of the Go players would have expected that databases of human games would be valuable training material for machines instead of humans:

> I learned mathematics because others gave their time and knowledge freely, and I wanted to do the same for the next generation. The possibility that a student would go on to do something I could not do was part of the point. But I had imagined this as a continuation of a human activity. [...] I could not imagine treating this knowledge as something to be guarded.

But soon after, AlphaZero was trained purposefully without human games in the training data. The "extractive" training was sufficient to show that a certain machine learning model worked, but unnecessary to produce a machine that performs beyond the level of humans.

For coding agents I imagine it is similar: humans introduce so many subtle bugs, and they're only subtle relative to human cognitive capacity. I'm sure subtle mistakes pass peer review in mathematics too, even if it's generally more rigorous.

What I'm getting at is that labs have demonstrated that a certain model architecture is capable of producing mathematics at a (super)human level, and their extractive methodology was sufficient, but possibly not necessary. You can fight in court whether their methodology is against the law, but it would be naive not to look beyond that, which is my main gripe with the AHM statement the author refers to [1]

Fortunately the author of this article has a more nuanced view:

> I can understand the anger, but I am not sure that withdrawing from AI is the answer

[1] https://www.ahmath.org/statements

See https://github.com/openai/PrimeGaps186

Looking at this I'm reminded of https://en.wikipedia.org/wiki/Polymath_Project, in particular "Yitang Zhang's 2013 breakthrough on bounded prime gaps, eventually lowering the upper bound on the gap between consecutive primes from 70,000,000 down to 246".

It depends entirely on your trust model. If you just want to be able to compile a rust compiler on a new platform that only has a C compiler, you wouldn't care. If you worry about a Thompson-style trojan horse, then you want to be able to audit all sources in the bootstrap chain.

Some idealistic projects like live-bootstrap go a step further and don't even allow generated sources in the full source bootstrap chain, even if they are readable in principle, because the xz debacle showed that a configure script, which is also readable in principle, can contain a backdoor. In those projects you could probably still bootstrap Eurydice from sources, and then do the rust -> c translation of the rust compiler as an ordinary build step, before compiling it with a bootstrapped C compiler.

If it's readable C, this sounds great for a full source bootstrap of the rust compiler.

The cost of the N-S disproof was estimated to be $15,000,000 whereas a ChatGPT Pro subscription costs $500.

It might as well happen, similar to how AlphaGo was superseded by AlphaZero, at some point a model might produce better math if it's trained through self-play where it poses its own problems, instead of looking for open problems in literature.

Another trick I have found useful is to do integration testing with coverage enabled. One agent creates tasks for subagents that run the application with coverage enabled, it merges the reports, and based on that it comes up with new tasks for subagents, repeat until coverage no longer moves.

I've updated the site and wrote a blog post here: https://stoppels.ch/2026/10/03/wake-me-up-when-ai-can.html

Did you also notice the complex emergent behavior of "418 I'm a teapot"?

(OP here) It was fun as long as it lasted ;) I'll leave it open for a few more days, but already it has enough votes for an interesting results page.

The `-j` is meant for the top-level invocation only, and the $(MAKE) pattern is standard.

The `+` or $(MAKE) "tricks" to ensure the jobserver is inherited in submake and any other subprocess are no longer needed in gmake 4.4 (from 2022) because it defaults to a FIFO instead of pipes. The author should just upgrade gmake :).

What if the tool is more advanced, like an optimizing compiler: `g++ -O3 -march=native -x c++ - <<EOF ... EOF`

If the compiler invocation is sufficiently slow, the llm could consider outputting a binary directly?

For all we know matrix multiplications are a faster way to generate optimized machine code than branchy sequential compiler code with tons of heuristics and passes.

Yeah, "standardizing" change IDs would make it much easier to develop further tooling around it. In particular decentralized review is something that I'd be interested in.

For example, if GitHub is down, that would not be a blocker to access review comments or to do reviews. And maybe you could push your reviews to a GitLab mirror if you want a UI.

An even simpler "sandbox" is to create a separate user and home dir for your LLM.

The reason is that their primary source of truth (traditional database) and their search index (elasticsearch) are out of sync.

The issues/pulls pages used to be showing the data from the primary data source, and then they changed it so everything is search, including the basic props is:pr and state:open.

5 years is great, but I'm sure in Norway they advertise "no flip" / "no turn" / "single-sided" mattresses as a feature too ;)

With sufficient competition, the incentives of companies would change if consumers would be willing to rent instead of owning products. Then planned obsolescence is not to their benefit.

If it is a skill, it's something that can be learned by both humans and LLMs.

Strongly reminiscent of God of the Gaps [1]

[1]: https://en.wikipedia.org/wiki/God_of_the_gaps

Wouldn't AI make the field of mathematics more ambitious? In software development it feels that way: there are often tasks I can take on that would have been too risky in 2025, because it was unclear if they were worth it. Now you generate a prototype and can make much better judgement calls what is possible and what is worth pursuing.

Mathematics is more than establishing arbitrary facts (although some look like curiosities), it's also defining what interesting research directions are and establishing common language/notation. I think that will stay relevant?

The maths community is now in the antithesis phase, synthesis will take a while ;)

Lee Sedol said in an interview that "losing to AI, in a sense, meant my entire world was collapsing. ... I could no longer enjoy the game. So I retired", and I think there will be folks in the mathematical community who would feel the same when the solutions pages to hard problems are suddenly available.

But on the other hand, people learned a lot from chess engines. After decades of chess computers beating humans, there was still a renewed interest in watching Leela beat Stockfish, with many people trying to understand the strategy Leela used.

If your happiness comes from grinding on a problem and making progress, the prospect of having to dig through a corpus of AI-generated proofs might be hard to swallow. But if you're willing to do that, you will still find beautiful things that only so many people can truly appreciate.

Great read, thanks for sharing

It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it).

To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?