Zulip Chat Archive

Stream: maths

Topic: Teaching with Lean

Kevin Buzzard (Feb 13 2019 at 15:10):

Patrick's formatter has made me start thinking about not teaching Lean to students, but teaching maths to students using the formatter. In fact I am even considering a situation where Lean code is hidden completely and the students can only see the tactic state, which is far less intimidating.

This made me realise the importance of notation. A student can understand Hn : n <= N but something like ha : is_limit a l is far harder for a mathematician to read. Is there unicode notation for limn→∞\lim_{n\to\infty} somehow?

Kevin Buzzard (Feb 13 2019 at 15:11):

@Patrick Massot could we even have something which processes the tactic state and turns is_limit a l into a LaTeX limn→∞an=ℓ\lim_{n\to\infty}a_n=\ell?

Reid Barton (Feb 13 2019 at 15:14):

You may be able to approximate this somewhat with notation, possibly?

Wojciech Nawrocki (Feb 13 2019 at 15:18):

You can definitely do something like 

constants (a l: Foo)
notation `lim`` n->∞ `a` = `l := is_limit a l
#check is_limit a l -- lim n->∞ a = l : Foo

alhough I don't know how well the equality notation will play with notation for eq. Maybe Lean 4's extensible parsers could make this better.

Kevin Buzzard (Feb 13 2019 at 15:19):

I am motivated to make it look as sexy as possible. Can I make the n -> infty as a subscript using unicode?

Reid Barton (Feb 13 2019 at 15:20):

Hmm, but this assumes the free variable is named n

Reid Barton (Feb 13 2019 at 15:20):

but I guess the original is_limit a l didn't even have an explicit free variable anywhere, so I don't know what to do about that

Wojciech Nawrocki (Feb 13 2019 at 15:23):

AFAIK Unicode only provides a predefined set of subscript characters and neither an arrow nor the infty sign seem to be among them.

Patrick Massot (Feb 13 2019 at 16:41):

Yes, unicode won't be good enough. But mathjax is good enough. However it will have to be a regex-based hack (until we get a Lean 4 structured tactic state).

Patrick Massot (Feb 13 2019 at 16:42):

My tool could filter the tactic state before displaying it and search and replace there

Kevin Buzzard (Feb 18 2019 at 22:28):

https://xenaproject.wordpress.com/2019/02/18/224/ -- me trying to tell kids aged 14-15 about inductive types ;-) It went OK! I think that next time I might try 15-16 though...

Chris Hughes (Feb 19 2019 at 00:02):

Why shouldn't your daughter be forced to learn about cosines?

Kevin Buzzard (Feb 19 2019 at 07:45):

Because she doesn't like maths

Last updated: Dec 20 2023 at 11:08 UTC