## Stream: new members

### Topic: modular arithmetic

#### Kevin Lacker (Sep 30 2020 at 15:32):

does mathlib or lean have a system for doing modular arithmetic, or the related theorems like fermat's little theorem? i can't find anything on the mathlib docs search, but i feel like i might be searching for the wrong thing

#### Kevin Buzzard (Sep 30 2020 at 15:33):

The equivalence relation on N/Z of being congruent mod n is called nat.modeq/int.modeq, and the quotient ring is called Zmod n.

#### Kevin Buzzard (Sep 30 2020 at 15:33):

What happens if you search there for Fermat?

#### Kevin Lacker (Sep 30 2020 at 15:34):

it kicks me to a google search, fermat site:https://leanprover-community.github.io/mathlib_docs

#### Kevin Lacker (Sep 30 2020 at 15:34):

and then the links on that google search are broken

#### Kevin Lacker (Sep 30 2020 at 15:35):

or at least the one mentioning number theory is

#### Kevin Buzzard (Sep 30 2020 at 15:35):

lol I wanted Fermat and got format

#### Kevin Lacker (Sep 30 2020 at 15:35):

was there formerly a page in the docs named field_theory/finite.html ?

#### Alex J. Best (Sep 30 2020 at 15:36):

We have docs#zmod and docs#int.modeq, with fermat being docs#zmod.pow_card and similar results in https://github.com/leanprover-community/mathlib/blob/master/src/field_theory/finite/basic.lean#L282

#### Kevin Buzzard (Sep 30 2020 at 15:36):

eew that's pretty nasty. Yes I think there was.

#### Kevin Buzzard (Sep 30 2020 at 15:36):

@Rob Lewis presumably we can't do much about google returning out of date links?

#### Bryan Gin-ge Chen (Sep 30 2020 at 15:36):

GitHub search is sometimes better than the site-specific Google search (which seems to be always out-of-date): https://github.com/leanprover-community/mathlib/search?q=fermat

#### Heather Macbeth (Sep 30 2020 at 15:37):

And there was a discussion a few days ago with some other forms of Fermat:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/p.20divides.20x-x.5Ep

#### Kevin Lacker (Sep 30 2020 at 15:37):

ah ok - src/field_theory/finite/basic.lean is the file i was looking for

#### Kevin Lacker (Sep 30 2020 at 15:38):

@Kevin Buzzard is there a sitemap? usually those prevent out of date links

#### Kevin Buzzard (Sep 30 2020 at 15:39):

Bryan will I'm sure know. I'm not involved with the website.

#### Bryan Gin-ge Chen (Sep 30 2020 at 15:39):

The docs are generated by the code in the doc-gen repo. I don't think we're generating a site map yet.

#### Rob Lewis (Sep 30 2020 at 15:39):

Kevin Buzzard said:

Rob Lewis presumably we can't do much about google returning out of date links?

No, AFAIK there's nothing we can do. There is a sitemap. This change happened a couple days ago.

#### Rob Lewis (Sep 30 2020 at 15:40):

https://leanprover-community.github.io/mathlib_docs/sitemap.txt

#### Kevin Lacker (Sep 30 2020 at 15:41):

is there a robots.txt pointing to the sitemap? i dont see one

#### Kevin Lacker (Sep 30 2020 at 15:41):

so google might not know to pick up the sitemap?

#### Rob Lewis (Sep 30 2020 at 15:42):

It's registered in the Google search console.

#### Kevin Buzzard (Sep 30 2020 at 15:42):

So is it worth adding a "github search" option to the docs search?

#### Kevin Buzzard (Sep 30 2020 at 15:42):

On this occasion it fared better than google.

#### Kevin Buzzard (Sep 30 2020 at 15:43):

~~what with the quanta article coming out tomorrow morning¬¬

#### Rob Lewis (Sep 30 2020 at 15:43):

The builtin docs search doesn't use Google anymore either, it's strictly based on declaration names.

#### Kevin Buzzard (Sep 30 2020 at 15:43):

Right, which was why we couldn't use it to find Fermat's Little Theorem

#### Kevin Lacker (Sep 30 2020 at 15:44):

the search on https://leanprover-community.github.io/mathlib_docs/ sent me to a google search

#### Rob Lewis (Sep 30 2020 at 15:45):

Oh, that's sneaky. Actually clicking the search button has a different effect than hitting enter...

#### Kevin Buzzard (Sep 30 2020 at 15:45):

with currently broken links

#### Kevin Lacker (Sep 30 2020 at 15:45):

hitting enter did nothing, so i clicked the search button

#### Bryan Gin-ge Chen (Sep 30 2020 at 15:45):

We definitely want both since I think the declaration name search doesn't see docstrings / comments.

#### Kevin Buzzard (Sep 30 2020 at 15:46):

The point is that currently neither option works when searching for "Fermat"

#### Rob Lewis (Sep 30 2020 at 15:46):

I think this is very far from an ideal user interface, but yeah, it should be easy enough to redirect the button to GitHub.

#### Kevin Buzzard (Sep 30 2020 at 15:46):

whereas github search does work

#### Kevin Buzzard (Sep 30 2020 at 15:46):

Hitting enter takes you to format because no Fermat is in any name in mathlib

#### Kevin Lacker (Sep 30 2020 at 15:47):

probably if you just do nothing and wait, google will fix up the links before too long

#### Kevin Lacker (Sep 30 2020 at 15:47):

presumably you aren't changing the URLs around all that frequently

#### Bryan Gin-ge Chen (Sep 30 2020 at 15:47):

Unfortunately, we are...

ha

#### Kevin Buzzard (Sep 30 2020 at 15:48):

we move fast and break things

#### Kevin Lacker (Sep 30 2020 at 15:49):

what does the docs search do when I hit enter - does it just send me to the #1 result?

#### Kevin Lacker (Sep 30 2020 at 15:49):

for example, i'm searching now for "totient" - i'm trying to figure out if the theorem that phi(ab) = phi(a)*phi(b) is anywhere

#### Kevin Lacker (Sep 30 2020 at 15:50):

but if i type "totient" and hit enter, the search just takes me right to the page for nat.totient, which is like just one of the many places that do things with totients

#### Adam Topaz (Sep 30 2020 at 15:51):

This file has a bunch of stuff:
https://github.com/leanprover-community/mathlib/blob/master/src/field_theory/finite/basic.lean

#### Adam Topaz (Sep 30 2020 at 15:51):

But I don't see the fact that $\varphi$ is multiplicative.

#### Rob Lewis (Sep 30 2020 at 15:52):

Neither Google nor GitHub is obviously better. Google is a good fuzzy search that keeps you in the doc pages but can be outdated. GitHub is up to date but it's a stricter search and you can't easily get from GitHub back to the docs.

#### Rob Lewis (Sep 30 2020 at 15:53):

"Awesome doc search" was supposed to be a bachelor thesis project this spring but, uh, world events got in the way. It's still in the pipeline.

#### Adam Topaz (Sep 30 2020 at 15:53):

But digging through the imports, there's this too:
https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/totient.lean

#### Adam Topaz (Sep 30 2020 at 15:54):

You can also do a git grep for totient

#### Adam Topaz (Sep 30 2020 at 15:54):

That will tell you all the files where it appears.

#### Kevin Lacker (Sep 30 2020 at 15:55):

kind of an unrelated question - can you guys actually read code like: (λ m hm, have hm : m < n / d ∧ gcd (n / d) m = 1, by simpa using hm,
mem_filter.2 ⟨mem_range.2 \$ nat.mul_div_cancel' hd ▸
(mul_lt_mul_left hd0).2 hm.1,
by rw [← nat.mul_div_cancel' hd, gcd_mul_left, hm.2, mul_one]⟩)

#### Kevin Buzzard (Sep 30 2020 at 15:55):

@Kevin Lacker there's a cemetary at the bottom of https://leanprover-community.github.io/lean_projects.html, a web page which I can never find the link to.

#### Kevin Lacker (Sep 30 2020 at 15:55):

because you remember what everything like mem_filter, mem_range, gcd_mul_left, you know what those are

#### Kevin Lacker (Sep 30 2020 at 15:56):

or is it more like, this stuff is write-once, read-never

#### Kevin Lacker (Sep 30 2020 at 15:56):

the compiler accepts it, therefore it's a success

#### Kevin Lacker (Sep 30 2020 at 15:56):

i'm just trying to figure out what standards to hold myself to here

#### Kevin Buzzard (Sep 30 2020 at 15:56):

Do you understand how to use the infoview?

#### Kevin Buzzard (Sep 30 2020 at 15:56):

Here's an interesting exercise.

#### Kevin Lacker (Sep 30 2020 at 15:56):

well i'm on github so there's no infoview

#### Kevin Buzzard (Sep 30 2020 at 15:57):

You don't read code on github

that's crazy

#### Kevin Lacker (Sep 30 2020 at 15:57):

okay I am starting to understand your culture better

#### Kevin Buzzard (Sep 30 2020 at 15:57):

that's like watching a movie with the sound off

#### Bryan Gin-ge Chen (Sep 30 2020 at 15:57):

#4312 defines multiplicative functions, though at a first glance it doesn't have the totient.

#### Kevin Buzzard (Sep 30 2020 at 15:57):

you download the project and you read the code with the help of the infoview

#### Kevin Buzzard (Sep 30 2020 at 15:58):

You put your cursor just after the := and you can then just keep hitting the right arrow key and you can see everything that's going on

#### Kevin Buzzard (Sep 30 2020 at 15:58):

you can see the state of the machine at that point

#### Kevin Lacker (Sep 30 2020 at 15:59):

isn't that like saying, we don't read code, we just step through it in the debugger

#### Kevin Lacker (Sep 30 2020 at 15:59):

so basically yes, the code is unreadable

#### Kevin Buzzard (Sep 30 2020 at 15:59):

I can read that code

#### Kevin Buzzard (Sep 30 2020 at 15:59):

can you post it again but using triple backticks so it gets highlighted correctly?

#### Kevin Buzzard (Sep 30 2020 at 16:00):

and I'll read it to you

#### Kevin Lacker (Sep 30 2020 at 16:01):

can you just explain this part of the code: coprime_div_gcd_div_gcd

#### Kevin Lacker (Sep 30 2020 at 16:01):

do you know what that does offhand, or no

#### Kevin Buzzard (Sep 30 2020 at 16:01):

if you were running this code on your computer you could just hover your mouse over that and something would pop up telling you what that meant precisely

#### Kevin Lacker (Sep 30 2020 at 16:02):

        ⟨b / d, mem_filter.2 ⟨mem_range.2 ((mul_lt_mul_left (show 0 < d, from hb.2 ▸ hb.2.symm ▸ hd0)).1
(by rw [← hb.2, nat.mul_div_cancel' (gcd_dvd_left _ _),
nat.mul_div_cancel' (gcd_dvd_right _ _)]; exact hb.1)),
hb.2 ▸ coprime_div_gcd_div_gcd (hb.2.symm ▸ hd0)⟩,
hb.2 ▸ nat.mul_div_cancel' (gcd_dvd_right _ _)⟩))


#### Kevin Buzzard (Sep 30 2020 at 16:02):

but because I can "speak a bit of Lean" I can guess what that means

#### Kevin Buzzard (Sep 30 2020 at 16:02):

it is an assertion that two numbers are coprime, and one number is being called "div_gcd" and the other is also called "div_gcd"

#### Kevin Lacker (Sep 30 2020 at 16:03):

i literally laughed out loud. not sure why

#### Kevin Buzzard (Sep 30 2020 at 16:03):

and so I would conjecure that this was the statement that if a and b were numbers in some suitable system which had a notion of gcd

#### Bryan Gin-ge Chen (Sep 30 2020 at 16:03):

(I think Kevin L said that he uses emacs, so instead of hovering he might have to hit some ctrl- ctrl- keybind.)

#### Kevin Lacker (Sep 30 2020 at 16:03):

it's not clear to me which buffer is the "info view" in emacs-world

#### Kevin Buzzard (Sep 30 2020 at 16:03):

then it's the assertion that a/gcd(a,b) and b/gcd(a,b) were coprime

#### Kevin Buzzard (Sep 30 2020 at 16:04):

the lean infoview is a more convenient version of any of the emacs buffers, for beginners at least

#### Kevin Buzzard (Sep 30 2020 at 16:05):

unless it's now possible to have the infoview in emacs, which it might be knowing this lot

#### Adam Topaz (Sep 30 2020 at 16:05):

One thing that's maybe not so clear is the notation ▸, and the infoview would tell you precisely what this means.

#### Kevin Lacker (Sep 30 2020 at 16:05):

the emacs docs and vscode docs don't seem to use any of the same terminology, so i can't quite tell how they compare

#### Kevin Buzzard (Sep 30 2020 at 16:06):

If you're a beginner and are reading a lot of code, then having it running locally is essential because then every question you have about the code can be answered.

#### Kevin Lacker (Sep 30 2020 at 16:06):

but basically I am getting it. the code is not readable in the traditional software engineering sense that people just look at some code and know what it does. the standard practice is to be analyzing everything with the editor tooling, and also in practice to write code once and never change it

#### Mario Carneiro (Sep 30 2020 at 16:06):

It is a bit unfortunate but I think that unreadability without the goal view is always a side effect of tactic based proofs

#### Mario Carneiro (Sep 30 2020 at 16:07):

I think what we really need is a viewer that provides this information in a static document format

#### Mario Carneiro (Sep 30 2020 at 16:07):

Metamath proofs are basically that

#### Kevin Lacker (Sep 30 2020 at 16:07):

it makes sense, though, you never have a proof that you want to just alter its behavior a little bit. once a proof is valid, you're done, you never need to change it

#### Adam Topaz (Sep 30 2020 at 16:07):

I don't know about that... I've tried to read some agda proofs before, and found it more difficult than reading tactic blocks

#### Mario Carneiro (Sep 30 2020 at 16:07):

Oh term mode proofs as well

#### Mario Carneiro (Sep 30 2020 at 16:08):

I didn't mean to make a contrast against term mode there

Ah ok.

#### Mario Carneiro (Sep 30 2020 at 16:08):

If you look at a giant lambda calculus term without the types it's bewildering

#### Mario Carneiro (Sep 30 2020 at 16:08):

That's the basic motivation behind #explode

#### Mario Carneiro (Sep 30 2020 at 16:09):

the real explanation is the sequence of types that appear, the proof term is just a serialization mechanism for the inference rules being applied

#### Johan Commelin (Sep 30 2020 at 16:09):

I guess we can try to run lean-formatter against the entire repo. Not sure how many CPUs it will burn though.

#### Mario Carneiro (Sep 30 2020 at 16:10):

If we can get lean running on the web this could be done dynamically on a per-proof basis

#### Mario Carneiro (Sep 30 2020 at 16:10):

although some engineering would be needed to make it snappy without having to work from scratch every time

#### Mario Carneiro (Sep 30 2020 at 16:12):

ideally you could just load up the oleans and be ready to step through the text

#### Rob Lewis (Sep 30 2020 at 16:33):

Kevin Buzzard said:

Kevin Lacker there's a cemetary at the bottom of https://leanprover-community.github.io/lean_projects.html, a web page which I can never find the link to.

@Kevin Buzzard now linked at the bottom of https://leanprover-community.github.io/ and in the "Community" memu.

#### Patrick Massot (Sep 30 2020 at 16:36):

Kevin Lacker said:

it makes sense, though, you never have a proof that you want to just alter its behavior a little bit. once a proof is valid, you're done, you never need to change it

Of course we change proofs very often when we generalize stuff or alter definitions slightly. There is no problem at all.

#### Scott Morrison (Oct 01 2020 at 02:21):

I think a good rule of thumb for deciding when inscrutable proofs are okay is the following:

• if it is the sort of fact that, if you started explaining it to a mathematician, they would stare at you blankly and not understand that there was even anything to explain, you can make the Lean proof as terse and inscrutable as you like
• if anyone could reasonably be expected to have to stop and think about a step, ideally it is possible to reconstruct that step from looking at the proof (admittedly, perhaps with the goal view)
• if you'd actually say it in a research paper or textbook, it deserves a human-readable comment (even if just a doc-string re-explaining the type of the def or lemma`)

Last updated: May 12 2021 at 04:19 UTC