Making Mathlib into an interactive encyclopedia of math?

Stream: lean4

[Mr Proof]

I am reading about all these things people are constructing in the FLT thread about "quaternion modular forms" and "adeles" (whatever they are). And think that while people are constructing the Mathlib wouldn't it be nice to also have more detailed explanations for the topics? So that it could be of use not only for professional mathematicians but also for people learning math. (And perhaps for professional mathematicians to learn new areas of math).

I think it would be nice if on top of Mathlib which is a kind of dictionary of theorems, there could be a more encyclopaedia type approach also. Where the different topics were explained in a more in-depth way. Which could have interactive examples. And automatic formatting into Latex equations. This might also help in organising and finding lemmas.

(Kind of like the MathWorld website but backed by Lean) Maybe even a Wiki approach.

Is this something that is currently been done? Or that may be done in the future? Just my 2 cents.

[Jireh Loreaux]

#mil

[Kevin Buzzard]

Have you seen https://imperialcollegelondon.github.io/FLT/blueprint/Quat_alg_project.html and https://imperialcollegelondon.github.io/FLT/blueprint/Adele_miniproject.html ? Those are my attempts to explain quaternionic modular forms and adeles to people with a general mathematical background. I do not see any reason to explain anything in any greater depth because it would make the FLT write-up of infinite length; if you want more details then just refer to standard number theory and algebra undergraduate and MSc level textbooks.

[Mr Proof]

That is great and all, I think perhaps my idea of "general mathematical background" is probably a bit different to yours. I was thinking more of something accessible to someone at undergraduate to graduate level.

And maybe that is not possible as some concepts are necessarily built upon things which require several years of graduate study to understand.

To be more precise I think someone who understood what a quaternion is, and what modular forms are, may still struggle on statements like "Recall that a quaternion algebra over K  is a central simple K-algebra of K-dimension 4."And symbols like $D^\times$. (Someone can correct me if these things are taught at undergraduate level these days). OK, well these aren't difficult concepts, it's more the unfamiliar language.

So, in conclusion although it goes against the point of the project which is to produce a highly formalised and precise language. My opinion is that it may also benefit from a few "dumbed down" explanations in the sense of "mathematical outreach".

[Mr Proof]

Jireh Loreaux said:

#mil

Yes exactly this! :grinning_face_with_smiling_eyes: (It took me a while to realise this was a link)

Would benefit I think if the project to automatically convert Lean syntax to Latex ever gets completed.

Also, would be cool if it was interactable like a notebook. But I am asking too much :pensive:

[Patrick Massot]

You’re not asking too much, unless you also have a deadline… All this will exist at some point in the future.

[Mr Proof]

That's great. No, I don't have a deadline, just happy to see it all coming together nicely. :+1: