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).
IMO Grand Challenge
71–75 of 75 posts
Re: IMO Grand Challenge
#72I'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
#73Is Reid Barton back to doing academic mathematics?
Re: IMO Grand Challenge
#74I thought Reid Barton was at RenTech? He's back in academia?
Re: IMO Grand Challenge
#75Earlier quoted context omitted.
> 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.
Uni adds a much more axiomatic and formal approach.