481–490 of 531 posts
Earlier quoted context omitted.
Spending all your money on extremely quickly depreciating graphics hardware and model training
And model training isn't putting money back into the business?
Well, time to set down the glass beads and dive into a an alpine lake.
There are hopefully still some Ludi to play before doing that, Magister.
I would love to see a theory in the spirit of Guerino Mazzola work, but for (combinatorial) games.
Earlier quoted context omitted.
The answer is we don't really know [0]: > In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid However it's a bit dif…
What are the chances that a small C program uncovers a bug in the C compiler, maybe in its type checker? What are the chances that a very large C program uncovers a bug in the C compiler?
Earlier quoted context omitted.
> Note that this proof while impressive does not add any value to mathematics as a human pursuit. I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
I enjoyed this Terence Tao post the other day. The relevant quote is > one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?" And later > But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided…
Earlier quoted context omitted.
To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.
The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main...
Earlier quoted context omitted.
What would it cost to make a team of mathematicians do the same?
Buzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.
Its like using AI to do your homework in the middle of a class. Yes, in the short term, that solves the problem of completing your homework. But it creates an entirely new problem of if you never did the homework how do you intend to pass the rest of the class or the remainder of college curriculum? A lot of cheaters ... don't.
A project has a long term path for permanent progress across an entire field. An oracle answers a question, sometimes cryptically, then progress in the field permanently ceases.
The value of a research project to determine if a Turing Machine halts with a T or a F on the tape is, to some extent, did it get a T or an F on the tape, but much more so the value is the tendrils of the rest of the field of mathematics pushing into the project at the start and then pushing out to enrich the rest of the field of mathematics at the end.
On the other hand if you have a project to run that Turing machine and see if it ever halts with a T or F as the proof, the result is completely sterile and WRT advancement of the rest of the field the actual result is kinda irrelevant. No postdoc is going to take the skills learned and move on to a position somewhere else and apply those new skills toward advancing something else in the field or describing a new goal or new way to look at the world. We'll get a popular science article about "oh it turns out the answer is indeed 'T'" and thats it. Sterile.
Personally I always thought the theorem proving turing machine would indeed terminate with a "T" and indeed it did. That's nice, and I bet the result settled a lot of bar bets. Aside from that, it will have minimal impact on progress in the field compared to the human project that's actually advancing the field.
Possibly people will be able to parse the 13 million lines of whatever into useful progress elsewhere in the field, possibly not. It'll be hard to get funding for it. OTOH its early days. Might end up useful in the end.
Earlier quoted context omitted.
I enjoyed this Terence Tao post the other day. The relevant quote is > one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?" And later > But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided…
That seems narrow minded. Theres both "learnings directly related to the thing studied" and "learnings downstream from the thing studied". If you imagine mathematics being a huge sudoku puzzle of unknowns you are trying to fill in, each previously empty square you are able to fill in (or gain a smaller bound on) has implications in all sorts of other areas.
Also, that Sudoku analogy doesn't sound right to me. Math progress is more complex than that.
> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
>> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. > Pretty insane. I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook: --- Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then H ∨ N = HN = { hn | h ∈ H, n ∈ N }. --- This says that the subgroup closure of H and N, the smallest s…
I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".)
My algebraic friends surely know it and they would never include it in a paper because everyone knows it.
I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it is a nice PR for beguiners.
Earlier quoted context omitted.
Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.
ok, you now added some unknown inference system in addition to zfc