The https://prooftoys.org/ website presents logic and basic
mathematics of the real numbers. It includes a practical embedded
deductive system for learners whose background may be just ordinary
high school mathematics. The site includes:<p>1. An introduction to logic through pictures, basically interactive
Venn diagrams with explanation. This is a point of view on
propositional calculus.<p>2. A brief presentation of the rules of the logic of "simple type
theory" at a raw beginner's level.<p>3. A number of completely rigorous simple proofs, some in pure logic,
and some about real numbers, starting from the classic "complete
ordered field" axioms that define the behavior of real numbers. The
proofs are all done by computer from the ground up using the logic
and axioms (with a handful of gaps). The proofs are all available
for reading online, down to any level of detail, interactively, and
at the reader's discretion.<p>4. A web-based tool that lets you build and edit your own proofs.<p>I am seeking user input on the site, and will gladly answer all kinds of
questions as far as I am able.