Hi, thanks for creating this Game. It is quite interesting and it has proven invaluable to me at learning Lean4.
I am now working on this problem set.
I wish to factor out two, but I actually had a typo and did this instead unfortunately.
have factor : 2 * a n - 2 * L = 4 * (a n - L) := by ring_nf
-- of course, what I wanted was to multiply by 2 on the RHS.
-- we don't have access to `ring`, which when applied as a tactic to the same input fails.
Very confusingly, what Lean4 does is to introduce an unprovable goal. This isn't necessarily captured in the UI, which I think could be confusing from the pedagogic point-of-view.
PS - Lean is very hard!
I learned Lean3 about 5 years ago or so, and remember struggling with ring, ring_nf, norm_num, bound, linarith because they all did quite overlapping things. Thank you for making this and believing in your vision. A gamified system is quite a nice way of motivating students to learn how to use Lean.
One thing I will remark is that I cannot imagine learning real analysis at the same time that I am learning Lean, as I would struggle to draw a partition between learning the mathematics, and learning the Lean language. I must commend the students who are so young and yet in your lectures they demonstrate a stark willingness to grapple with the material.
Hi, thanks for creating this Game. It is quite interesting and it has proven invaluable to me at learning Lean4.
I am now working on this problem set.
I wish to factor out two, but I actually had a typo and did this instead unfortunately.
Very confusingly, what Lean4 does is to introduce an unprovable goal. This isn't necessarily captured in the UI, which I think could be confusing from the pedagogic point-of-view.
PS - Lean is very hard!
I learned Lean3 about 5 years ago or so, and remember struggling with
ring,ring_nf,norm_num,bound,linarithbecause they all did quite overlapping things. Thank you for making this and believing in your vision. A gamified system is quite a nice way of motivating students to learn how to use Lean.One thing I will remark is that I cannot imagine learning real analysis at the same time that I am learning Lean, as I would struggle to draw a partition between learning the mathematics, and learning the Lean language. I must commend the students who are so young and yet in your lectures they demonstrate a stark willingness to grapple with the material.