Something or other, whatever!

Christian Lawson-Perfect's homepage

Lean Blockly

I had a thought about using Blockly to construct proofs, which would be translated to Lean code for evaluation.