3 ms·
This is a significantly harder problem than winning gold in IOM. A large part of it is figuring out how to represent some of the relevant ideas in Lean at all.
by rcxdude 1y ago
This is a significantly harder problem than winning gold in IOM. A large part of it is figuring out how to represent some of the relevant ideas in Lean at all.
- Davidzheng 1y agoI disagree. I think it's a sequence of a huge number of modular moderately hard tasks each much easier than a hard IMO question.
- markusde 1y agoIMO problems are stated in and solved by math a high schooler could understand. Getting the definitions right (one of the harder parts of mechanizing proofs IME) is a different beast altogether.