Post #1366383
2023-10-24 04:34 UTC
I haven't had time to install Lean so in my (very few) spare moments, I've been playing @xenaproject's Natural Number Game. At first I unknowingly played the Lean3 version. As someone who has been using automated deduction tools for two decades, I found some of it very confusing and unnatural. There were several times I had a relevant lemma and a hypothesis and all I wanted to do was a good old fashioned modus ponens, but I couldn't get it to work so I had to proceed in a roundabout way.
Then I found the Lean4 version, https://adam.math.hhu.de/#/g/hhu-adam/NNG4 , still under development. Maybe struggling with the older version primed my subconscious, or maybe it's the newly rewritten instructions, but now it all makes much more sense to me.
Having handled Peano arithmetic, I am clearly ready to fit my elementary proof of Fermat's Last Theorem into the margin of my text editor.
Replies (1)
-
@xenaproject@mathstodon.xyz 2023-11-25 18:27
@ProfKinyon The Lean 4 version of the game had `apply ... at` which was missing in Lean 3. All of the function and proposition world thing was to really try and explain that logical implication can be thought of as a function, and all of that was an attempt to make students understand how `apply f` could turn the target of `f` into its source and thus argue in a direction which they don't normally think about. In the Lean 4 version I have dumped this completely, there are no abstract propositions at all, it's all numbers, and we can argue the normal way (forwards) with `apply at` and it's much easier.