111–120 of 526 posts
I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.
Big Bang - history of the understanding of space and the universe
Code book - history of the maths of ciphers
Haven’t read them for years but I’ve been meaning to again
Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
I'm so curious what happens to this project that intended on proving FLT by 2029 now the project: https://imperialcollegelondon.github.io/FLT/
Earlier quoted context omitted.
It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
LLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?
About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture
Wiles’s proof will remain a mystery to me.
I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.
Also recommend his other books! Big Bang - history of the understanding of space and the universe Code book - history of the maths of ciphers Haven’t read them for years but I’ve been meaning to again
> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1. At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.