I'm a high school sophomore and I have been interested in Interactive Theorem Proving for a year or two. I found it extremely hard for my peers (lack of knowledge in mathematical logic, type theories or functional programming) to learn how to use these mainstream coding-based proof assistants (e.g. Lean 3/4, Coq, Isabelle and so on). Understanding the logical foundations of them (e.g. HoTT, CiC, HOL) is far more difficult.
(I have learned Lean+Coq a bit, which already took me a long time to read tutorials, digest and practice. It's a steep learning curve with high cost and long cycle!)
I'm wondering if anyone have (or planned to) developed a graphical front-end for a/some proof assistant(s) that is easy to learn (even by my peers, just like Scratch).
As checking the correctness of maths reasoning is a typical daily task of teachers and students in secondary schools, if there exists a user interface that wraps the existing system into easy-to-learn applications, maybe these kinds of advanced and cutting-edge technologies can benefit basic education a lot.
(But I haven't seen any such attempt.(applying ITP to secondary maths education) Is this because no one has tried it, or is there another reason?)
I know the The Incredible Proof Machine, which is possibly the easiest prover to learn. But it's also too simple to tackle complex maths concepts.
I know the Holbert, which claimed designed as an educational tool. But it seems that Holbert is more suitable for Programming Languages courses. And I think its GUI for ITP is not straightforward enough.
Other graphical provers I know, including HolPy, homotopy.io and this one, can't meet the requirements to be used in basic maths education as well. (in my opinion)
From my perspective, combining an IPM-like flowchart editor, Scratch-like tactic builder and Lean's mathlib will form an ideal ITP GUI for teens.
