Blockly with Lean

Stream: general

[Archibald Neil MacDonald]

I'm not a mathematician. Just a programmer who found the natural numbers game scratched a logic puzzle itch. This is a WIP to combine the lean server with the Blockly GUI.

2021-08-24_01-07-42.mp4

[Patrick Massot]

Fun! Is there anything we could play with?

[Archibald Neil MacDonald]

:working_on_it: Not yet! I'll see if I can get something interactive by the end of the week.

[Jörg Hanisch]

Is there any progress in this direction?

[John Mercer]

Thanks so much for sharing @Archibald Neil MacDonald ! I had no idea Blockly existed! This experience is the goal for building ProofFlow in TMGP using React Flow library (experimenting with both a tree vs cascade view) across formal languages as well as a proof game using generated datasets from Wolfram FindEquationalProof. This is a perfect example where we're trying to provide the organization and full-time employment opportunity to take a "side itch" and give someone a pathway for full-time role to build a real production product experience within a unifying platform.
image.png
image.png

[Eric Wieser]

Sounds like we should exploit the new Lean4 widget powers to put confetti in the infoview!