Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

IMO Grand Challenge

imo-grand-challenge.github.io

Post reply on HN
Print view View original

51–60 of 75 posts

Re: IMO Grand Challenge

#51

Post by NieDzejkob »

eru wrote: post #30
throwaway-ai-ai wrote: post #22

Earlier quoted context omitted.

Suppose your assertion about this problem being easy was true. Most research papers in Math / Theoretical CS are 1 page. So it's only a factor of 50 "more complex." Then, we should be able to encode open problems / conjectures in Math / Theoretical CS into Lean, run this brute fore approach, and have it start auto generating new publications. To the best of my knowledge, no one has done this yet.

Well, the IMO problems are constructed with a solution in mind. Also, who says that efforts goes up linearly with size? (Not necessarily agreeing with lordnacho here, just saying that your argument ain't a good one.)

That's a good point. If we assume each line of a publication is just applying an axiom, the complexity of such a search is clearly exponential in the length of an article. I feel like this wouldn't be better if we dropped the assumption.

Re: IMO Grand Challenge

#52

Post by knzhou »

OscarCunningham wrote: post #49
knzhou wrote: post #47

Earlier quoted context omitted.

I think this illustrates one of the preconceptions this challenge is meant to work against. Namely, people think of coordinate bashing as "computational" and purely synthetic/geometric solutions as "insightful". But there's no reason that a computer would find the second way more difficult. After all, synthetic geometry is just another system of rules, like ordinary algebra. Us humans might fall back on coordinate ba…

The current situation doesn't reflect that though. We have a algorithm (Gröbner bases) for doing coordinate bashes which is guaranteed to succeed, whereas as far as I know we don't have an analogous algorithm in terms of synthetic geometry (other than the direct translation of coordinate bashing).

Sure, but I don't think theoretical guarantees are that important in practice. When I solve math problems, I don't personally use methods with such guarantees. Mathematica has certain guarantees for evaluating integrals, but that really doesn't help when it chokes for an hour on one. In practice what matters is computational complexity, and how well heuristics can help you narrow down your search space. And here IMO geometry problems have the enormous advantage that one knows there exists a short, purely synthetic solution.

Re: IMO Grand Challenge

#53

Post by pfortuny »

OscarCunningham wrote: post #40
saagarjha wrote: post #17

Earlier quoted context omitted.

IMO problems are generally proof-based and don't always lend themselves well to brute force solutions using analytic geometry.

The kind of problems I'm thinking of are those like 2 and 6 on this year's IMO. You have a bunch of points, lines and circles in some configuration and you have to prove that some condition holds. So you assign symbols to represent the coordinates of each of these points and you represent each fact you are told about them by some equation. The condition you are trying to prove is also represented by some equation. Af…

Yes: those problems will boil down to: do some functions (polynomials) belong to an ideal (maximal, usually)?

Grobner it and you are done.

Re: IMO Grand Challenge

#55

Post by sdenton4 »

OscarCunningham wrote: post #49
knzhou wrote: post #47

Earlier quoted context omitted.

I think this illustrates one of the preconceptions this challenge is meant to work against. Namely, people think of coordinate bashing as "computational" and purely synthetic/geometric solutions as "insightful". But there's no reason that a computer would find the second way more difficult. After all, synthetic geometry is just another system of rules, like ordinary algebra. Us humans might fall back on coordinate ba…

The current situation doesn't reflect that though. We have a algorithm (Gröbner bases) for doing coordinate bashes which is guaranteed to succeed, whereas as far as I know we don't have an analogous algorithm in terms of synthetic geometry (other than the direct translation of coordinate bashing).

tho tbh i'd love to see an NLP project for turning high school geometry problems into grobner basis problems, and solving them there.

Re: IMO Grand Challenge

#56

Post by pirocks »

I'm curious as to whether LEAN is the right choice for this. LEAN is rather hard to parse, and complex, as a consequence of being designed for use by humans. Perhaps specifying the problem(s) in a small superset of first order logic would be better?

Re: IMO Grand Challenge

#57

Post by dan-robertson »

saagarjha wrote: post #36
eru wrote: post #32

Earlier quoted context omitted.

I guess it depends on what you mean by university level mathematics. Terrence Tao definitely says that doing university math changed his approach to these problems. See https://terrytao.wordpress.com/books/solving-mathematical-pr...

> I guess it depends on what you mean by university level mathematics. Calculus.

This definitely depends on the country. There’s a reasonable amount of calculus in high school (strictly sixth form) mathematics in the U.K. The things one tends to see in university begin with (abstract) algebra and analysis with some “calculus” topics being things like vector calculus, more generic R^n->R^m calculus and contour integration.

Re: IMO Grand Challenge

#58

Post by th-th-throwaway »

throwaway-ai-ai wrote: post #19
saagarjha wrote: post #14

Earlier quoted context omitted.

I was nowhere near anywhere good enough to participate in an IMO officially, but judging by the types of problems they ask I'm not super optimistic. This might come back to bite me, but I'd predict that EC2 won't be around when this is solved.

I would guess that a computer beats humans on the IMO before a computer beats humans on the IOI/ICPC -- but also think that the latter would have far greater impact.

Have you seen this paper? https://openreview.net/pdf?id=ByldLrqlx

You can see some of the simpler programs that can already be generated on page 12.

Re: IMO Grand Challenge

#60

Post by woopwoop »

OscarCunningham wrote: post #40
saagarjha wrote: post #17

Earlier quoted context omitted.

IMO problems are generally proof-based and don't always lend themselves well to brute force solutions using analytic geometry.

The kind of problems I'm thinking of are those like 2 and 6 on this year's IMO. You have a bunch of points, lines and circles in some configuration and you have to prove that some condition holds. So you assign symbols to represent the coordinates of each of these points and you represent each fact you are told about them by some equation. The condition you are trying to prove is also represented by some equation. Af…

There is a Mathoverflow thread [0] about this. Discussion in the comments expresses skepticism because olympiad questions usually involve questions about choosing specific real roots of polynomials, not just arbitrary roots. The discussion there mostly suggests using some principles in real algebraic geometry, but these seem to be too slow and complicated to use in practice at this time.

[0] https://mathoverflow.net/questions/337558/automatically-solv...

Post reply on HN