Knowing how to use a new powerful tool is definitely a valuable asset. I hope that my wordplay didn't come across as downplaying that; I genuinely meant it as a compliment to them!
Not a Lean expert but some of the proof tactics used to prove are probably novel? Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?
>Not a Lean expert but some of the proof tactics used to prove are probably novel
Maybe. But they're in 32 millions lines of Lean. How do you find the needle in the haystack ?
>Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?
If OpenAI was truly serious about improving maths (and not jerking themselves off), they'd have also used Prove2Me (and contributed their results back), which would have done that. Each part of the proof combines into a larger graph, that everyone can reuse. Note that Anthropic isn't better there: yes, they used Prove2Me, but as far as I know they haven't contributed back to it, and just shat out 10 million lines and a good luck everyone.
Leaf dumps out a proof object that can be verified to be correct. Absent a bug in the verifier, you can trust it, probably more than you can trust a human-produced proof. This is why Lean was a thing even before AI.
A lot of good repos (CLIs, frameworks) had 'tree' unicode directory structure with like ├──, └──, and │ , as well as emojis for passing/failed tests and README docs maybe a unicode arrow or two, but LLMs absolutely overuse it.
I don't know why chatbots prefer → over -> so much. It's becoming a countersignal compared to the old terminal customization era, where arrow ligatures were a signal of effort.
In times when software eng teams push for maximizing token usage, Tao's public view is to encourage verification, limit AI use for tasks that have real-life consequences and prevent low-effort papers that exhaust the review pipeline?
He also focuses on training the next generation of mathematicians and prioritizing the process of slow digestion of results, which to me sounds very.. reasonable?
Taos public view is to engagement farm and he'll swap to the new nfts or crypto when this is done because once you go down this road theres no going back with the lifestyle creep
sure, but the prior poster's "joke" was that Germans are bad at English and refer to overhead projectors as "beamers" when in reality the entire English-speaking academic world refers to slide decks as Beamers because they all use the Beamer software to generate their slide decks
