No, I don't want to see the prompt. Yes it has some llm tics, but it's clear that he went back and forth before arriving at this. Why would I be interested in the transcript?
well here's the thing - i did! i smelled the 50/50 and then gave it to Pangram. Neither my nose and Pangram are 100% accurate, but when they both get a hit I'm pretty confident.
yes and? someone sharing the details of an extremely popular project is super cool. comments like this will not encourage more people to share more cool things.
I'd be ecstatic if more people used AI to share more cool things they've done. that'd be awesome. more of this blog post please.
But very little of the author shines through here, at least after the intro. I, too, would like to hear more about how someone built stuff, but this is not it.
Yes, I let the AI generate the diagrams from the code, a bit like tools such as "Doxygen" would in the olden days.
I was a bit pushed for time, and didn't feel inclined to try making the diagrams myself.
Still, I agree that they're a bit "slop adjacent". However, I thought they would be better than nothing for someone trying to get their bearings.. and I did iterate on them a bit to get them to be more useful than the initial clanker efforts!
LLMs are sometimes stupid and get confused when you change the files without them knowing. So asking them to do even simple things keeps the context in sync.
Plus you get a bonus random line "methods are all on the top" in the commit message that makes no sense to anybody.
We understand the proof (most math from all of history) -> We understand how the proof was made (computer-assisted proofs like the four-color theorem) -> We have to trust the computer's explanation for how the proof was made (some LLM proofs)
Is that really a problem? The only risk in a Lean proof is the LLM finding a bug in multiple kernels (2 with the standard setup) that would let it add a new theorem without legitimately proving it. If you have reasoning traces or send a second model to look at the proof you can easily detect that and file a bug report.
For the rest you only need to check that the formal problem statement matches the actual problem and the proof is not using extra axioms. That's easy to check manually or with a simple script.
Many mathematicians care about understanding the method and the tools used more than the result. LLMs have a large advantage in memory and reading speed, you can feed them the entire internet and published literature at training time, and then make them check dozens of papers in a few minutes at runtime. They might not be very creative, but they've seen that obscure 1990's theorem in the training data that happened to use an idea that might just work again.
Reading the LLM's 12 MB lean output is a bit like trying to maintain a codebase that has been fully vibe-coded as a single giant file, by hand. Even if it's possible in principle, no one is going to enjoy that.
I understand the spirit of what you're saying, but "unassisted humans" isn't a good yardstick. There's hardly anything "unassisted" humans understand today... We require plenty of assistance from computer tools in most scientific discoveries.
This is based on a 108 page prose paper that the repository links to. Of course, that's a very difficult paper as well, I don't know how many people would be qualified to read and digest it, but they do exist.
That reminds me that people who hear the word for butterfly (Schmetterling) in German for the first time usually think it sounds extremely violent. Ok, then again, "butterfly" sounds slightly disgusting if you think about it. But TIL that they actually have a similar root: the "Schmetter-" doesn't come from smashing, but from "Schmetten", a word derived from the Slavic "smetana" (cream). Apparently butterflies got their name from the popular belief that witches could turn into butterflies to steal milk or cream (and probably also other dairy products?).
reply