Zulip Chat Archive

Stream: maths

Topic: Teaching with Lean


view this post on Zulip 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?

view this post on Zulip 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 limnan=\lim_{n\to\infty}a_n=\ell?

view this post on Zulip Reid Barton (Feb 13 2019 at 15:14):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Feb 13 2019 at 15:20):

Hmm, but this assumes the free variable is named n

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Feb 13 2019 at 16:42):

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

view this post on Zulip 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...

view this post on Zulip Chris Hughes (Feb 19 2019 at 00:02):

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

view this post on Zulip Kevin Buzzard (Feb 19 2019 at 07:45):

Because she doesn't like maths


Last updated: May 11 2021 at 16:22 UTC