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.

"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)

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.

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.

But the conceit of the IMO has always been that the problems are drawn from a very limited selection of fields, which are/were commonly taught in high schools around the world. No need for complex numbers, calculus, abstract algebra, or trigonometry (though any of these may end up used in an alternative solution).