пока каменный цветок не выходит (положу в комментарии, как это выглядит) — поделюсь ссылкой на компьютерную игру: https://adam.math.hhu.de/#/g/AlexKontorovich/RealAnalysisGame

(первое впечатление: это невыносимо, непонятно как кто-то может в этом формализовывать какие-то содержательные доказательства… но мб у вас получится лучше)