471–480 of 564 posts
Earlier quoted context omitted.
No. Funny how these discussions too often devolve into semantics lol.
Funny how people don't understand basic logic. If it is a proof in a logic, and the machine checked that proof, it is a proof, no matter that no human actually understands it. A human doesn't need to understand the proof, they just have to understand why the proof is a proof.
This means we may need to remove or replace the Olympiad..It has no practical significance..Winners never contributed to any major scientific breakthroughs.
[1]: https://www.aeaweb.org/articles?id=10.1257/aeri.20190457
Earlier quoted context omitted.
Funny how people don't understand basic logic. If it is a proof in a logic, and the machine checked that proof, it is a proof, no matter that no human actually understands it. A human doesn't need to understand the proof, they just have to understand why the proof is a proof.
Well... assuming a human made no mistakes setting up that logic.
> ... but whenever IMO is brought up, a caveat should be put out: medals are awarded to 50% of the participants (high school students), with 1:2:3 ratio between gold, silver and bronze. That puts all gold and silver medalists among the top 25% of the participants. yes, it is true, but getting to the country specific team is itself an arduous journey, and involves brutal winnowing every step of the way f.e. regional m…
Source: a friend who got silver on the IMO
Earlier quoted context omitted.
> Everyone's busy watching Magnus Carlsen. Actually, I was looking up Elo ratings of the top computer chess players, and learned that it is not that trivial to compare these, due to differences in hardware requirements and whatnot.
Are you arguing computer chess players are as popular as human chess players?
This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn bas…
Earlier quoted context omitted.
… no? After the LaTeX output, I told stock GPT4o that the answer was "all even integers", and asked for the statement in Lean. I had to make two changes to its output (both of which were compile-time errors, not misformalisations), and it gave me the formalisation of the difficult direction of the problem. Both changes were trivial: it had one incorrect (but unnecessary) import, and it used the syntax from Lean 3 ins…
> I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this. Why?
Earlier quoted context omitted.
Link isn't working for me can you summarize. What i heard ten years ago was that 1pt is quite common for a significant progress
Yeah, the progress has to be quite significant, no points are awarded for trivial observations. Thus scores are usually bimodal around 0 and 7. In the linked stats you can see that 1 point for P3/P5 was less common than full score on other problems.
Earlier quoted context omitted.
Only slightly more general. It only works for games that are zero-sum, deterministic, have no hidden information, and discrete game state and moves. Other examples include connect-4.
So finding Lean proofs can be conceptualized as a zero-sum game? Another basic requirement is that valid moves / inference steps and the winning condition can be efficiently verified using some non-AI algorithm. Otherwise there would not be a reward signal for the reinforcement learning algorithm. This is different from answering most natural language questions, where the answer can't be checked trivially.