4 ms·
Yeah, they do often require a lot of math. It's just a restricted set of topics. The IMO doesn't do any calculus or anything beyond calculus like real analysis,
by lacker 6y ago
Yeah, they do often require a lot of math. It's just a restricted set of topics. The IMO doesn't do any calculus or anything beyond calculus like real analysis, topology, etc. It does have a lot of geometry problems that use geometry that typically isn't in the American curriculum, and it has topics like number theory that aren't really in a standard high school curriculum either. But the topics are restricted so that they are pretty close to understandable by someone who has just done well in a standard high school mathematics curriculum.
Here's an example. For the problem they include in the article:
Let n be an integer greater than or equal to 3. Prove that there is a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area.
This is a whole lot easier if you're familiar with Pick's Theorem, which gives you a formula for the area of a polygon whose corners are integer lattice points. In particular, any three integer lattice points define a triangle with rational area. So all you have to do is find n points that aren't colinear with each other and have irrational distance, and you'll solve the problem.
Technically, you could do this without Pick's Theorem, because you'll be able to find an equivalent formula for the area of these triangles. But it's much easier if you do know Pick's Theorem, and that's the sort of thing that you typically don't pick up in standard high school math, but you would pick up if you were practicing a bunch of different Olympiad-type problems.
- logicallee 6y agoHa, 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 agohttps://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.