5
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • $\begingroup$ My two cents is that logic is inherently hard. Sure, making the installation simpler or code completion better will improve learning experiences. But the core difficulty is just there, and once you get past that the skill is yours. $\endgroup$
    – Trebor ♦
    Dec 30, 2022 at 11:18

1 Answer 1

Reset to default
1
$\begingroup$

It is quite old and I’m not sure it still runs, but you can look at MathXpert. It is a GUI proof assistant for algebra and calculus.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I have downloaded it and had a try. I think it's more a CAS with step-by-step interaction than a "proof assistant". It lacks extensibility. But I like its "selection+choose_operation" style. Maybe It can be a reference for further ITP-GUI development. Thanks! $\endgroup$
    – Chesium
    Dec 31, 2022 at 8:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.