111–120 of 288 posts
I am utterly fascinated by the amount of comments here from engineers that clearly have zero experience with mathematics making utter fool of themselves by claiming to know better than mathematicians what their jargon is/means, how publishing works/should work, etc… I try not to go down the route of “hn was better before!” but… jeez, do better, people. What happened to this community, there used to be some effort to…
Smart move by them for waiting until the drama died down before making a completely neutral statement. The statement is so sterile they don't even mention who solved it. The word "OpenAI" doesn't appear at all.
I really like this style of writing for some reason. Not sure how to put it but it’s a rare combination of a vague post and confidence
It's easy to get caught in the details of today. Our skepticism, our distrust, our loathing. For people, for companies.
This is a nice pull in the other direction, a silver lining. In the grand scheme of things, we're solving these frontier problems: Somebody did it and that's amazing.
That's what it was all about when this started of in 2000.
Earlier quoted context omitted.
Someone made a 'proof' of the Collatz conjecture that way in Lean. However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
> However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions. I don't think this is true in general. It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us. In lean, the structure of a situation like this is that your single branch with a goal divides into multiple br…
Earlier quoted context omitted.
You don't need to read the lean proof for that, only the statement.
You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
I am utterly fascinated by the amount of comments here from engineers that clearly have zero experience with mathematics making utter fool of themselves by claiming to know better than mathematicians what their jargon is/means, how publishing works/should work, etc… I try not to go down the route of “hn was better before!” but… jeez, do better, people. What happened to this community, there used to be some effort to…
What did you expect? Degree of BS increases together with the population.
Earlier quoted context omitted.
Who cares about the prize and the outdated methods? OpenAI and Anthropic might have 3 millennium problems by December
https://xkcd.com/605/
OpenAI needs to solve another to shut down the (baseless) plagiarism allegations. Anthropic wants blood because OpenAI sniped the last one from one of Anthropic's researchers.
It's a matter of pride for both companies. More results will come out soon.
In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory. However, after reading the open letter sign…
OpenAI spent many multiples of the prize money in just a few days to get there and even if one solves a problem in the traditional way, that person is most likely already an accomplished professor at a reputable university where a million dollars doesn't mean as much as the eternal fame that comes with it.
Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results. As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough
Earlier quoted context omitted.
Completely misleading. This is all you need to read and understand for Anthropic's FLT formalization: import Mathlib import Theorems.Thm_fermat_last_theorem /-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/ theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_o…
Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.