Lean for the Inept Mathematician

Stream: new members

[Huỳnh Trần Khanh]

grant huynhtrankhanh commit rights too :joy:

[Arthur Paulino]

Julian Berman said:

Will set up github pages too perhaps

Your sphinx integration lib would come in handy, I'd say

[Julian Berman]

Now we perhaps race to see who writes the first one ha.

[Julian Berman]

Yeah quite possibly, I may look at reviving it (for now I suspect it would sink a bit of time to get it in there because what's missing at the minute is automatic ref generation and without that life is a bit hard)

[Julian Berman]

Perhaps after we have an article or two

[Arthur Paulino]

what format are you thinking? blog?

[Julian Berman]

I was assuming markdown files a la Jekyll blog for the minute

[Julian Berman]

But open to whatever of course

[Huỳnh Trần Khanh]

let's use VuePress, it's quick and it's pretty :heart_eyes:

[Huỳnh Trần Khanh]

but hey, I have commit rights anyway so I'll commit a boilerplate real quick :joy:

[Arthur Paulino]

let's commit to other branches and open PRs to master :D

[Julian Berman]

Also maybe no bikeshedding (myself included) on format until we have a post :D

[Eric Taucher]

I requested a split of this topic.

[Arthur Paulino]

I think gh pages is a great format. I have an almost finished script that can turn lean files into md files. it's an extremely simplified version of alectryon

[Julian Berman]

That woudl be awesome, especially because we'll likely have to run the lean code to make sure it works with mathlib -- so something like that is probably an even better idea

[Arthur Paulino]

will get it up and running right after my dayjob shift :+1:

[Huỳnh Trần Khanh]

https://github.com/Julian/lftim/tree/someone-is-quicker-than-me

this thing is also very easy to use!!! you just need to write some markdown files and vuepress will take care of the rest :joy: the default theme is already neat enough so we don't need to change it, what is the point anyway :joy:

[Huỳnh Trần Khanh]

then we just need to use netlify to deploy the site! ez pz :joy:

[Arthur Paulino]

either way, md files seem to be a sweet spot

[Huỳnh Trần Khanh]

great! :joy: we already have a boilerplate!!! now let's write an article :joy: it's just a markdown file anyway, so easy :joy: what should we write now?

[Julian Berman]

Writing up your stars and bars is probably not a bad idea FWIW

[Eric Taucher]

For those looking for stars and bars

[Arthur Paulino]

Alright, I'm free now. Let me translate this javascript code to python. Should be easier to use

[Julian Berman]

I'm likely to find a movie and head to bed soon, but I started on a post (for math I know nothing about which I pulled from the "December in Mathlib" blog post) -- so there's some initial paragraphs here: https://github.com/Julian/lftim/commit/7b0f977549cd912f0f1f5bf5daf4e28785beb3d0 on lattice ordered commutative groups. Tomorrow I'll probably read through the (reasonably short file) but if anyone feels like adding to that, commenting on it, or whatever, go for it :)

[Arthur Paulino]

The script is almost working. Then we will be able to just write everything in lean and the MD files will be generated automatically.

Also, maybe, this deserves a separate stream so we can talk without worrying about spamming lots of people

[Huỳnh Trần Khanh]

hello? so what will we use? vuepress or jekyll? i prefer vuepress because it's easier to use for me though, and its default theme is very neat

[Huỳnh Trần Khanh]

here's my blog post :joy: https://github.com/Julian/lftim/blob/second-entry-unless-someone-beats-me-to-it/_posts/2022-01-07-Stars-and-bars.md

[Arthur Paulino]

I don't have experience using vuepress with GH pages

[Huỳnh Trần Khanh]

Arthur Paulino said:

I don't have experience using vuepress with GH pages

me neither. but I have experience using VuePress with Netlify :joy: the whole process is generally pretty straightforward

[Arthur Paulino]

I'd say let's make use of the page that GitHub offers for free this way we don't need to have spread content

[Arthur Paulino]

With GH pages, you just push a commit and the site updates accordingly

[Arthur Paulino]

But Jekyll or VuePress, I don't know. I only have experience with Jekyll. I'm open to learn but I am comfortable with whatever Julian chooses

[Huỳnh Trần Khanh]

2-1. 2 people prefer Jekyll, so Jekyll it is then :joy:

actually Netlify watches every commit on the GitHub repo and runs the build command automatically so the user experience should be the same :joy: but I respect your preference :joy:

[Huỳnh Trần Khanh]

:joy: no objections right? or should we wait for Julian to be online

[Huỳnh Trần Khanh]

🦗 ok everyone is asleep 💤💤💤 I'll leave this chat :joy: I'll be back when people are online again!

[Julian Berman]

I think we should write a few and then decide about tooling, until then minimal work necessary is just Jekyll. But yeah let's just write em first :)

[Arthur Paulino]

Alright, after some interruptions, I was finally able to get it done. The script turns this:

/- asd asd -/
def qq := 1

/-!
## eee

* aaa
* bbb
-/

def ttt := 5

Into this:

asd asd

```lean
def qq := 1
```

## eee

* aaa
* bbb

```lean
def ttt := 5
```

[Arthur Paulino]

We just call it by, for example, $ python lean2md.py src _posts, and it will iterate on all lean files inside src and produce their respective markdown files (with the same name except for the extension) inside _posts

[Arthur Paulino]

https://github.com/Julian/lftim/pull/1

[Huỳnh Trần Khanh]

inept mathematicians rejoice! I don't speak Python but I still understand the general logic of your code :joy: how much time did you spend on debugging :joy:

[Arthur Paulino]

Not much... I already had written something similar in javascript that does the same thing

[Julian Berman]

Nice. Sounds great, better than what I was doing copy pasting from files!

[Arthur Paulino]

If we want we can also make Jekyll link to the respective .lean file so it's easier for the reader to download it and follow along. But it's just an extra

[Huỳnh Trần Khanh]

haha, Donald Knuth invented literate programming and now we're doing something similar :rolling_on_the_floor_laughing:

[Huỳnh Trần Khanh]

sorry for the stale joke but I couldn't help it

[Julian Berman]

Huỳnh Trần Khanh said:

here's my blog post :joy: https://github.com/Julian/lftim/blob/second-entry-unless-someone-beats-me-to-it/_posts/2022-01-07-Stars-and-bars.md

You should PR this maybe for comments so we merge it! But it may also be nice to describe the normal stars and bars proof before you talk about how it's not the one Lean uses, I think it's cute, but that's just me.

[Arthur Paulino]

Julian Berman said:

I'm likely to find a movie and head to bed soon, but I started on a post (for math I know nothing about which I pulled from the "December in Mathlib" blog post) -- so there's some initial paragraphs here: https://github.com/Julian/lftim/commit/7b0f977549cd912f0f1f5bf5daf4e28785beb3d0 on lattice ordered commutative groups. Tomorrow I'll probably read through the (reasonably short file) but if anyone feels like adding to that, commenting on it, or whatever, go for it :)

While reading it, I noticed that it might be nice to have some sort of prelude, that is, a list of pre-requisite items that the reader should familiarize with before being able to fully understand the post. This is taking into consideration the fact that we're targeting inept mathematicians :D

I think it's a bit less scary than finding out strange/new concepts in the middle of the text. And it might as well expose ideas for next posts, with the intent to cover up the prelude topics

[Julian Berman]

Yes I thought about doing that, so I'm glad you did too :P will push me to do it.

[Julian Berman]

Did you find that to be the case?

[Julian Berman]

(That I mentioned something specific without explaining it? Just curious if I managed to)

[Arthur Paulino]

Julian Berman said:

Did you find that to be the case?

It was the case for me :smiley:
The advantages of having ourselves as targets hehe

This is my main problem when reading Wikipedia. The queue of things to know grows as I am reading the texts and it is really hard to manage in my head

[Yaël Dillies]

Same here. That's why I have 100 tabs open...

[Julian Berman]

Ha oy, yes understood. Eventually I clear out my 100 tabs and make believe that means I read them. Probably not the best approach :), but yes very good point.

[Arthur Paulino]

In practice, the difference is that by following this prelude approach, the reader can decide whether to go on or not just by glancing at the pre-requisites. This contrasts with realizing that it's actually too much to take in right now in the middle of the way

[Arthur Paulino]

This is a nice introspection experiment. My first stab will be at something way more basic like inj/surj/bijectivity of functions :thinking:

[Arthur Paulino]

Huỳnh Trần Khanh said:

here's my blog post :joy: https://github.com/Julian/lftim/blob/second-entry-unless-someone-beats-me-to-it/_posts/2022-01-07-Stars-and-bars.md

I agree with Julian about the post. It would be nice to have an explanation of the concept behind the proof. Maybe even with a simple example. I'd argue that the concept/intuition is at least as important as the proof itself for inept people like myself :upside_down:

[Eric Taucher]

When I first saw mention of ourselves as targets it made no sense to me. Now seeing it used in context a few times I take it that it means the goal is not to cover all of Math but only the math in MathLib (Lean 3). Is this the thinking to be associated with that phrase?

This then raises the question if this will cover only MathLib for Lean 3 and/or MathLib4 for Lean 4? It took me a more than a week when I came here to learn the there there was more than one MathLib for Lean.

[Ruben Van de Velde]

My understanding was that the authors consider themselves to be the "inept mathematicians" they are writing for

[Eric Taucher]

Ruben Van de Velde said:

My understanding was that the authors consider themselves to be the "inept mathematicians" they are writing for

I considered that but then I, currently being one of the inept mathematicians (related to Lean), can't even write anything about Lean if it brings along any mention of Math as noted in my earlier post.

[Stuart Presnell]

I think the idea is something like "write for your recent self". If you've just figured something out (e.g. how some proof works, or what's going on in some particular file in mathlib) then you could write an explanation that summarises your understanding. The target audience — the person you should imagine you're explaining this to — should be someone of about the same ability as yourself who hasn't just gone through the process of figuring it out. That is, you should write the article that you wish you could send back in time to your earlier self to save you that effort!

[Julian Berman]

And I think this likely means we'll have articles at slightly different levels from each other, but roughly corresponding to the group of us, none of whom are anything resembling grad-school. PhD or research mathematicians, so at a more digestible level for our average level of understanding.

[Eric Taucher]

Side quest of mine is to understand the emoji use here. What does :100: mean?

[Julian Berman]

None of the emoji mean anything. I used it just now to mean 100% (i.e. strong thumbs up).

[Julian Berman]

the goal is not to cover all of Math

By the way -- I think it's fine to cover something not in mathlib -- it will just mean you get to write the Lean code all on your own. But probably that will happen exactly when there's some nice piece of math you learn that you want to share but mathlib has it in some crazy generalization you can't begin to understand.

[Stuart Presnell]

Julian Berman said:

but mathlib has it in some crazy generalization you can't begin to understand.

Yes, I think articles like this will be very valuable as a balance against the mission for maximal generality that guides mathlib. Naturally, mathlib doesn't want to prove a result specifically for ℕ if it holds for an arbitrary unique factorization monoid; but this tendency toward generalisation means that the statements that get formalised in mathlib can be a bit abstracted and remote from everyday mathematical experience. It will be really useful, then, to have articles that pull these theorems down to earth and make it easier to understand what they're doing and what they're for.

[Arthur Paulino]

You can even write something that's super basic, like showing that the square of odd numbers is odd. And you can make it awesome by writing it in a way that you wish someone had explained it to you. Then linking it with a Lean proof that resembles your reasoning

[Arthur Paulino]

For instance, something that I am very curious about: how the hack can one prove results about euclidean geometry in Lean? I makes no sense to me right now. Once I understand, I want to write about it. And explaining things always deepened my understandings

[Mario Carneiro]

It's not explicitly related to mathlib formalization, but you might find A formal system for Euclid's Elements interesting regarding the question "how to do diagrammatic reasoning in a formal system"

[Huỳnh Trần Khanh]

I made an attempt to explain the traditional stars and bars proof. wording might be awkward, please help me fix the article https://github.com/Julian/lftim/blob/0e949741fc7432e17c701cdddd7dc7f2b3070c36/_posts/2022-01-07-Stars-and-bars.md

[Julian Berman]

Cool! Will have a look in a bit if no one else does first.

[Arthur Paulino]

Loved the emojis! :smiley:

[Stuart Presnell]

Huỳnh Trần Khanh said:

I made an attempt to explain the traditional stars and bars proof.

Rather than launching straight into the quote from mathWorld, could I suggest that you start by first warming up the idea of n choose k and then introduce the notion of multisets? Even if the reader already knows this, it's always helpful to warm up the brain-circuits!

[Arthur Paulino]

That or adding to the "prelude" (so we don't need to regress too much)

[Stuart Presnell]

Also you might start with a smaller example, so the reader can more easily work out the solution for themselves to verify that they understand. Or even give a worked example like this:

If we have an alphabet a, b, c, how many multisets of cardinality 2 can we construct?
First, let's count the multisets that contain a.
If one element of the multiset is a then that leaves us with 3 possibilities for the other element, giving {a,a}, {a,b}, and {a,c}.
Now we also have to count the multisets that don't contain a.
These are {b,b}, {b,c}, and {c,c}. So there are 6 in total.

A small worked example like this will help the reader to sniff out the recursive formula for counting multisets.

[Stuart Presnell]

As in the example above, it might be better to use letters for the alphabet rather than numbers — then we don't have to switch between thinking about numerals that are counting things and numerals that are just symbols in an alphabet.

[Stuart Presnell]

Notice that there is another way to represent each multiset.

As an intermediate step, you might point out that each multiset is completely characterised by how many as it contains, how many bs it contains, etc. — i.e. by a list of numbers. In particular, the length of the list is the size of the alphabet, and the sum of the list is the cardinality of the multiset. So every multiset of size k over an alphabet of n symbols corresponds to a way of writing k as a sum of n natural numbers.

From there it's natural (but not obvious!) to move to another representation: we start with k stars and insert bars to partition them into n bins.

[Stuart Presnell]

I like the use of emoji, but it might be easier to see what's going on if the "bars" were something like :barber: rather than :chocolate:, so it's easier to see them as little dividers inserted between the :star:s.

Also, for some reason I think a sequence like :star::barber::barber::star::barber::star::barber: might be easier to comprehend as a first example.

Somehow this seems easier to think of as "three :star:s with :barber:s inserted between them" — but I can't explain why! :upside_down:

[Paul Lezeau]

Hi, I'd be quite interested in contributing a post or two on algebra when I find some time, could you give me commit rights @Julian Berman ? My GH username is Paul-Lez

[Julian Berman]

done and that would be awesome! I am still behind on getting to finishing mine so we are still at an ambitious 0 posts so far but we'll get there.

[Arthur Paulino]

@Paul Lezeau feel free to test the lean2md.py script. It might have some unknown bugs

[Julian Berman]

Yeah, it's going to get confused with leading and trailing whitespace I saw.

[Julian Berman]

But I think it's OK to work those out as we find them.

[Julian Berman]

(And in the interim if everyone just writes .lean files I think we're in good shape)

[Paul Lezeau]

Julian Berman said:

done and that would be awesome! I am still behind on getting to finishing mine so we are still at an ambitious 0 posts so far but we'll get there.

Great! Thanks:)

[Paul Lezeau]

Arthur Paulino said:

Paul Lezeau feel free to test the lean2md.py script. It might have some unknown bugs

I'll let you know if I find anything!

[Arthur Paulino]

Alright I wrote about graph coloring because graph theory is the topic I'm most familiar with in mathlib:
https://github.com/Julian/lftim/pull/3

The resulting markdown file can be seen here

[Arthur Paulino]

Does anyone know how to set a pre-commit git hook? The documentation around this feature is super shallow.

I want to set a hook that runs the python script and then calls git add on everything under md automatically. It's annoying when I forget to run the script before committing

[Henrik Böving]

you just put an executable file named pre-commit into .git/hooks, examples can be found in said directory of any git repository.

[Henrik Böving]

Docs about git hooks are available here https://git-scm.com/book/en/v2/Customizing-Git-Git-Hooks

[Arthur Paulino]

Wow, that was a lot simpler than I thought. Thanks!!

[Huỳnh Trần Khanh]

several minutes late :joy: in the JavaScript ecosystem husky is widely used

[Arthur Paulino]

@Henrik Böving will sh files work on Windows tho?

[Henrik Böving]

I dunno how exactly git determines what executable to call on windows but I'm rather sure it won't ship it's own thing but instead use the same mechanism windows uses to figure out what to use when you double click something. You are not forced to use .sh you can use any language you want.

[Huỳnh Trần Khanh]

Arthur Paulino said:

Henrik Böving will sh files work on Windows tho?

yes. just believe me :joy:

[Huỳnh Trần Khanh]

I don't know why but it works

[Huỳnh Trần Khanh]

don't believe me? you can believe stack overflow though https://stackoverflow.com/a/18278072

[Arthur Paulino]

:octopus:

[Huỳnh Trần Khanh]

Arthur Paulino said:

:octopus:

you should take my advice. use husky. this way the git hooks are actually present in the repository. otherwise the git hooks are only available on your own machine. works on my machine ftw :joy:

[Huỳnh Trần Khanh]

it's just a simple wrapper but it's tremendously helpful

[Huỳnh Trần Khanh]

whenever someone clones the repository, they can run npm run prepare and yayy, the hooks are installed!!

[Huỳnh Trần Khanh]

ok I'll help you set this up

[Huỳnh Trần Khanh]

it's a one time thing and it's pretty quick

[Huỳnh Trần Khanh]

just wait for a PR lol

[Huỳnh Trần Khanh]

https://github.com/Julian/lftim/pull/4

[Arthur Paulino]

I was thinking about making a makefile for it instead of adding node packages

[Arthur Paulino]

(trying to keep the repo as minimal as possible)

[Arthur Paulino]

Or maybe a Python script

[Yaël Dillies]

I love how you're managing to do everything but the core of the project :rofl:

[Arthur Paulino]

How come? We have three posts in the oven

[Yaël Dillies]

Just kidding :stuck_out_tongue_closed_eyes: but you do spend a lot of time on the non post stuff

[Arthur Paulino]

I love taking the chance to learn whatever

[Yaël Dillies]

I'm in no position to judge because I myself went on so many detours to do some of the stuff that's now in mathlib

[Arthur Paulino]

I mean, I'm not even in front of a computer

Plus, setting up some sort of environment for a "lean book" is something that I've been thinking about for a while, so I'm trying out some ideas that I had

[Arthur Paulino]

Also, coming up with a proper idea to write about is something that happens at random while taking a bath or doing dishes. I'm not a mathematician so it's not very natural to me :rofl:

[Henrik Böving]

I've been contemplating about teaching org-babel about Lean for a while but I have neither the elisp skills nor the time at the moment :(

[Arthur Paulino]

I had never heard of it. Looks interesting

[Henrik Böving]

It's a part of the emacs plugin org-mode which you can use as basically anything really (and I mean anything, you can generate websites from it, write lecture notes with LaTeX snippets in it, TODO list and time management stuff, table calculation program etc.) and one of its many features is org-babel which basically allows you to write snippets in $LANGUAGE in your document and evaluate them while compiling the document to TeX/HTML/Word/Whatever and print the output into the document.

So theoretically speaking it should be possible to teach org-babel about Lean and due to a feature called sessions also to simply chain multiple lean blocks into one logical program. But I have absolutely not clue how org-babel actually works internally :/

[Arthur Paulino]

@Julian Berman merged after following your suggestions :)
https://github.com/Julian/lftim/pull/3
And we got our first post on master :octopus:

[Huỳnh Trần Khanh]

I'm not entirely sure if it's worth adding node dependency just to set a pre-commit hook.

of course, no :joy: the PR should only be merged if you are willing to use more tools from the Node.js ecosystem, otherwise I can make another PR which achieves the same thing, without Node and npm. spoiler: it's also very simple :joy:

[Huỳnh Trần Khanh]

take a look: https://github.com/Julian/lftim/pull/5

[Eric Wieser]

FWIW I think you're misusing client-side git hooks as a CI step. Why not generate the markdown files on github from CI running on master, then have CI commit the result to gh-pages?

[Eric Wieser]

That's roughly how most of the leanprover-community repos work

[Arthur Paulino]

I don't know about the others, but I'd like to see the markdown file in the PR diff, which makes the reviewing process a lot more pleasant

[Eric Wieser]

Except you can't actually comment suggestions on the markdown, right, as they need to be applied to the lean files first?

[Arthur Paulino]

Yeap. Julian proposed something a bit similar: a GH action that pushes a commit to a branch as soon as the branch receives a commit from an user. This approach is a bit annoying because we'd need to pull multiple times while fixing things in the review process.

[Arthur Paulino]

But I like your solution more in the other end of the spectrum: completely detaching ourselves from looking at markdown files during review and just sticking to lean files.

[Arthur Paulino]

I think it is in fact a better solution. What about those who want to contribute by writing markdown files directly?

[Eric Wieser]

That works fine too, they can just be copied to the build. Just don't store lean and md versions of the same post

[Arthur Paulino]

That makes a lot of sense. I probably misunderstood Julian's idea in the first place? Maybe

[Eric Wieser]

CI that adds commits to the same branch it builds in response to changes to (as you interpreted Julian's suggestion) is rarely a good idea, even if you teach it not to infinite loop - it makes managing your git history annoying, especially for inept git users!

[Eric Wieser]

(and also violates "don't commit your build outputs")

[Arthur Paulino]

Alright, so I did misunderstand Julian's idea. Good to know!
Thanks for pointing that out

[Eric Wieser]

(I don't know whether you did or not - I didn't say you misinterpreted it)

[Huỳnh Trần Khanh]

(deleted)

[Julian Berman]

Mostly I am indifferent at this point about tooling :) there are many ways that work, but I care about getting some posts up first and then thinking about it -- which means I truly am OK with whatever anyone wants for now.

[Arthur Paulino]

Alright. I merged Huỳnh's PR because it does make my life easier for now :+1:

[Huỳnh Trần Khanh]

yes. Khanh is my first name

[Huỳnh Trần Khanh]

@Arthur Paulino how did you realize your mistake lol

[Arthur Paulino]

Huỳnh Trần Khanh said:

Arthur Paulino how did you realize your mistake lol

Julian PM'd me :smiley:

[Stuart Presnell]

Hi @Julian Berman , could I have access? I have a couple of ideas for articles that I might try to write up. My username is stuart-presnell

[Julian Berman]

Sent!