So I was wondering if it is possible to host math competitions in a way similar to Codeforces. The obvious difficulty would be checking the solutions, since they are normally written in a natural language, meaning they cannot be checked automatically (at least yet). However, there are programming languages/proof assistants such as [Lean](https://en.wikipedia.org/wiki/Lean_(proof_assistant)) allowing you to write mathematical proofs that can be verified by a computer. I am not actually familiar with any of them, so I have two questions:

1. Are these languages mature enough or can become mature enough in the nearest future to host math competitions similar to the style of Codeforces.
2. As far as I know, doing math on a computer is still quite a niche thing in the math community. Do you think such competitions could make it more popular?

My reasoning is that a working mathematician might be reluctant to start using Lean, since there is no immediate personal benefit. However, students would be more willing to try for the sake of competitions, and then continue using it in academia in the future.

My slow solution 291665439 to 2031D - Penchick and Desert Rabbit passes the system tests.

My submission 148630829 for 1646D - Weight the Tree.

Jury's answer and the checker comment for Test 6.