3 ms·
Suppose your assertion about this problem being easy was true. Most research papers in Math / Theoretical CS are < 50 pages, while many IMO problems have solut
by throwaway-ai-ai 7y ago
Suppose your assertion about this problem being easy was true.
Most research papers in Math / Theoretical CS are < 50 pages, while many IMO problems have solutions > 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.
- eru 7y agoWell, 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.)
- NieDzejkob 7y agoThat'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.
- oefrha 7y agoComplexity is a terrible measure of mathematical value. Length of exposition is even worse.