7
$\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$
2
  • 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$ Commented Dec 30, 2022 at 11:18
  • $\begingroup$ No exactly what you're looking for, but I've heard of Edukera which is basically a wrapper around Coq. $\endgroup$ Commented Feb 2 at 11:40

3 Answers 3

Reset to default
2
$\begingroup$

The proof builder tool and really the whole Prooftoys website that hosts it, is my personal ongoing effort to provide the kind of thing you are talking about. It has a point-and-click GUI, and presents proofs as a sequence of lines, each representing a proof step. Equally important, it has a significantly simpler logic than most proof assistants. It is built on simple type theory, as are some "research-grade" proof assistants, but also heavily emphasizes use of simple textbook-like proof steps.

Improve this answer
$\endgroup$
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$ Commented Dec 31, 2022 at 8:52
1
$\begingroup$

I am currently doing exactly what you asked for at Blakelock high school in Oakville Ontario. I have prepared about 20 activities and the students are eagerly working on them.

Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.