@tomkalei Beweisprüfer (kurz ITP, insb. Lean) sind immer mehr im kommen. Es gibt einige namhafte Mathematiker:innen, die gerade Lean auch in ihrer Forschung einsetzen. Terance Tao macht das und er prophezeit, dass Lean im Zusammenhang mit LLMs zu einer Art "vibe coding" mathematischer Beweise führt. Erst letzten Oktober wurde so ein formaler Beweis mit ChatGPT für ein 1000$-Erdős-Problem gefunden und auf arXiv gestellt: https://arxiv.org/abs/2510.19804v1 Wieso spielt ITP+LLM für dich offenbar keine Rolle?