modular arithmetic

Stream: new members

[Kevin Lacker]

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]

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]

What happens if you search there for Fermat?

[Kevin Lacker]

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

[Kevin Lacker]

and then the links on that google search are broken

[Kevin Lacker]

or at least the one mentioning number theory is

[Kevin Buzzard]

lol I wanted Fermat and got format

[Kevin Lacker]

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

[Alex J. Best]

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]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Kevin Lacker]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Kevin Lacker]

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

[Kevin Lacker]

https://leanprover-community.github.io/robots.txt not found

[Kevin Lacker]

so google might not know to pick up the sitemap?

[Rob Lewis]

It's registered in the Google search console.

[Kevin Buzzard]

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

[Kevin Buzzard]

On this occasion it fared better than google.

[Kevin Buzzard]

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

[Rob Lewis]

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

[Kevin Buzzard]

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

[Kevin Lacker]

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

[Rob Lewis]

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

[Kevin Buzzard]

with currently broken links

[Kevin Lacker]

hitting enter did nothing, so i clicked the search button

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Rob Lewis]

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]

whereas github search does work

[Kevin Buzzard]

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Bryan Gin-ge Chen]

Unfortunately, we are...

[Kevin Lacker]

ha

[Kevin Buzzard]

we move fast and break things

[Kevin Lacker]

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

[Kevin Lacker]

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]

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]

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

[Adam Topaz]

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

[Rob Lewis]

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]

"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]

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

[Adam Topaz]

You can also do a git grep for totient

[Adam Topaz]

That will tell you all the files where it appears.

[Kevin Lacker]

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]

@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]

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

[Kevin Lacker]

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

[Kevin Lacker]

the compiler accepts it, therefore it's a success

[Kevin Lacker]

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

[Kevin Buzzard]

Do you understand how to use the infoview?

[Kevin Buzzard]

Here's an interesting exercise.

[Kevin Lacker]

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

[Kevin Buzzard]

You don't read code on github

[Kevin Buzzard]

that's crazy

[Kevin Lacker]

okay I am starting to understand your culture better

[Kevin Buzzard]

that's like watching a movie with the sound off

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

you can see the state of the machine at that point

[Kevin Lacker]

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

[Kevin Lacker]

so basically yes, the code is unreadable

[Kevin Buzzard]

I can read that code

[Kevin Buzzard]

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

[Kevin Buzzard]

and I'll read it to you

[Kevin Lacker]

can you just explain this part of the code: coprime_div_gcd_div_gcd

[Kevin Lacker]

do you know what that does offhand, or no

[Kevin Buzzard]

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]

        ⟨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]

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

[Kevin Buzzard]

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]

i literally laughed out loud. not sure why

[Kevin Buzzard]

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]

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

[Kevin Lacker]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Lacker]

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]

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]

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]

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]

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

[Mario Carneiro]

Metamath proofs are basically that

[Kevin Lacker]

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]

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]

Oh term mode proofs as well

[Mario Carneiro]

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

[Adam Topaz]

Ah ok.

[Mario Carneiro]

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

[Mario Carneiro]

That's the basic motivation behind #explode

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Rob Lewis]

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]

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]

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)