281–290 of 564 posts
Earlier quoted context omitted.
I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?
> just fumbling its way around until it guessed correctly As opposed to 0.999999% of the human population who can't do it even if their life depends on it?
Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
magnus carlsen basically quit because computers ruined chess. As did kasparov. Fischer was probably the last great player who was unassisted by tools.
To what extent is the training and structure of AlphaProof tailored specifically to IMO-type problems, which typically have short solutions using combinations of a small handful of specific techniques? (It's not my main point, but it's always worth remembering - even aside from any AI context - that many top mathematicians can't do IMO-type problems, and many top IMO medalists turn out to be unable to solve actual pr…
The last statement is largely correct (though idk what the imo medalists that are unable to solve actual problems most mathematicians can't solve most open problems). But i kind of disagree with the assessment of imo problems--the search space is huge if it were as you say it would be easy to search.
In other words, how does AlphaProof fare on mathematical problems which aren't in the IMO style? (As such exceptions comprise most mathematical problems)
I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.
(/s)
I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.
C'mon you're meant to be re-configuring 3,292,329 line of YML for K8s. (/s)
I guess I should have pursued a PhD when I was younger.
The problems were first converted into a formal language. So they were partly solved by the AI
Yes and it is difficult for me to believe that there is not useful human analysis and understanding involved in this translation that the AI is helpless without. But that I suppose is a problem that could be tackled with a different model...
Earlier quoted context omitted.
The linked page says > While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized by the agent. However, it's unclear what initial format was given to the agents that allowed this step
So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?