3 ms·

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 tra

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)

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

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