Hacker News Reader

Comment by nnarek | Hacker News Reader

formal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it is very interesting how they initially formalized problem without including answer in it

View on HN

(You're talking to one of the people who was part of the project, which is why I took @ocfnash's answer as authoritative: they did not cheat.)

If they're talking to the people who are part of the project I'd hope the answer would contain detail and not expect to be taken as authoritative.

I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like

{Formal description of the set in question} = ?

And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above.

I doubt they would claim to solve the problem if they provided half of the answer.

> I doubt they would claim to solve the problem if they provided half of the answer.

Stranger things have happened

To be fair, that isn't half the answer it's like 99% of the answer.

They clarified above that it provided the full answer though.

The deepmind team has a history of being misleading. The great StarCraft 2 strategist bot is still in mind.

What’s the story with that bot? Always thought it was cool. Was that all smoke and mirrors?

I think maybe parent comment is referring to it essentially just employing a zerg rush but with the speed and reaction time of an AI? Not 100% sure... Unrelated, iirc the starcraft functionality was an early example of generalizing a pretrained NN, alphaGO, and showing that it could adapt to learn and defeat games across strategic domains, especially after it learned so much strategy from the most difficult, widely played, and most strategically-varied physical game available.

> I doubt they would claim to solve the problem if they provided half of the answer.

This falls under extraordinary claims require extraordinary proof and we have seen nothing of the sort.

Exactly, a problem and its answer are just different ways of describing the same object. Every step of a proof is a transformation/translation of the same object. It would be disingenuous to say that some heavy lifting isn't done in formalizing a problem but it seems that step is also performed by a machine:

"We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty."

I'm confused, is the formalization by Gemini or "manually"? Which is it?

Come up with many possible answers, formalize them all, and then try to prove or disprove each of them.

This is probably partially what they did idk why it's downvoted lol

its not clear if theorem is actual input formal definition, or formal definition was in different form.

Reply on news.ycombinator.com