3 ms·
https://imo-grand-challenge.github.io/ https://imo-grand-challenge.github.io/ For the challenge, they give the AI a formal representation of the problem in Lea
by deanmen 6y ago
https://imo-grand-challenge.github.io/ 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.
- logicallee 6y agothanks. 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?
- im3w1l 6y ago∀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.