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?
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.
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.