News for hackers. Stuff that matters.

A comment on At the International Mathematical Olympiad, computers prepare to go for the gold. Parent comment

Re:At the International Mathematical Olympiad, computers pre... by logicallee on Monday September 21, 2020 @06:24PM (#24549105)
Ha, Pick's theorem. Such hopelessly advanced problems (I'll give an example shortly) are well beyond what a cluster of ten thousand GPU's can solve today if trained for a thousand days on the types of math you've mentioned and then given a hundred hours to compute the answer to an infinitely, staggeringly and mind-bendingly intricate problem such as this one:

"Starting at 2, how many times must you double the number for the result to exceed 10?".

(Or a similarly trivial one.) Yeah. Really. Try it. They don't understand language at all. Just try to interact with any of the assistant or computational knowledge engines.

Here's what wolfram alpha gives you for that query:

Query:

Starting at 2, how many times must you double the number for the result to exceed 10?

Computed response:

1 | adjective | (especially of eyes) bulging or protruding as with fear 2 | adjective | appropriate to the beginning or start of an event 3 | noun | a turn to be a starter (in a game at the beginning)

[ Parent | on HN ]
Re:At the International Mathematical Olympiad, computers pre... by deanmen on Monday September 21, 2020 @07:02PM (#24549331)
https://imo-grand-challenge.github.io/

For the challenge, they give the AI a formal representation of the problem in Lean. To remove ambiguity about the scoring rules, we propose the formal-to-formal (F2F) variant of the IMO: the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof. We are working on a proposal for encoding IMO problems in Lean and will seek broad consensus on the protocol.

[ Parent | on HN ]
Re:At the International Mathematical Olympiad, computers pre... by logicallee on Tuesday September 22, 2020 @08:13AM (#24553559)
thanks. that's really not the IMO though, is it? coming up with a formal representation is a large part of the challenge, isn't it?
[ Parent | on HN ]
Re:At the International Mathematical Olympiad, computers pre... by im3w1l on Tuesday September 22, 2020 @01:34PM (#24557445)
∀n∈Z: n>=3 => ∃S∈(R^2)^n: [~∃p1∈S ∃p2∈S ∃p3∈S ∃a∈R: p1!=p2 & p2 != p3 & p3 != p1 & p1 + a(p2-p1) = p3] & [~∃p1∈S ∃p2∈S ∃a∈Z ∃b∈Z: |p1-p2| = a/b] & [∀p1∈S ∀p2∈S ∀p3∈S ∃a∈Z ∃b∈Z p1!=p2 & p2 != p3 & p3 != p1 => Area(p1, p2, p3) = a / b]

So far it's pretty much mechanical∗. The big question is how you will formalize Area(p1, p2, p3). Heron's could possibly make the problem much harder than cross product.

∗Although I may have made some or many mistakes.

[ Parent | on HN ]