A few days ago, I shared a link to this visual theorem proving system: http://incredible.pm/ It doesn’t have Dependent Type Theory yet, so it can’t quite do theorems about natural numbers yet. But it does go all the way to Simply Typed Lambda Calculus. I found it fascinating and have been solving the puzzles. Here’s an idea that it triggered: What if we could build physical Lego-like blocks that represent these kind of reasoning and their shapes and ports support syntax-less proofs? Wires can carry truth values just like this simulator and variables can be introduced with specific connector shapes. Bugs like cyclic reasoning etc can probably be detected with feedback/amplification etc. May be the idea is far-fetched but there are examples of people using physical programming blocks which are Turing-complete like Scratch and the block shapes naturally eliminate syntax errors and basic mistakes.

really love the idea of the shape of the blocks preventing errors. Would be super interesting to see if it also encourages exploration / curiosity. Maybe there’s a block you’ve never used before but it shares the shape with a block you’re familiar with, maybe you’d try it! I haven’t used this myself, but this product appears to use the same shapes as the physical blocks you’ve shared above — https://thunkable.com/#/

https://www.blawx.com/ is doing a domain specific version of it for legal

String diagrams come to mind https://ncatlab.org/nlab/show/string+diagram.

Sorin Lerner has a blocks-kind-of prototype for proofs in natural deduction. It's called "Polymorphic Blocks". Here is a link to a site where he talks about it: https://cseweb.ucsd.edu/~lerner/pg.html .

@Robin Polymorphic blocks was a fantastic share. I can't find the actual game but Sorin's talk was super-interesting. Thanks for sharing! @wtaysom I'll have to find a less technical treatment of string diagrams to understand them. 😁

That is oh so fair! Here's the least technical introduction I know. https://graphicallinearalgebra.net/

The polymorphic blocks game is available here: https://cseweb.ucsd.edu/~lerner/proof-game/

That is remarkably close to being amazing.

I am fascinated by the fact that I can use it, sort of, but I still don't know what I am doing, at all. There are some interface problems, and it doesn't scale without zoom, but there is something here, for sure.

Any teachable insights? I'm still playing it like a 3 year old 🙂 even with the notation turned on...

Yeah, I think I have it, now. The up shapes are propositions. The down shapes are conjunction and disjunction semicircle is conjunction, triangle is disjunction. Pink is the conclusion, yellow is the premises. Each contiguous set of blocks is an implication from yellow to pink. The extra blocks are rules of inference, and "extending" them just allows you to carry unrelated premises forward. Double clicking indicates that the premises show the conclusion for that implication.