Where to lookup math theories/conjectures etc.?

Stream: new members

[Eric Taucher]

Being a programmer first when any reference to a math theory, conjecture etc. is noted I instantly convert into a mental gap and continue, E.g. Hedetniemi's conjecture. While I can use Wikipedia to learn more about them, is there a better place to learn about them to connect the dots to make what I read make sense. I am not looking to get a degree in math but something that doesn't have me filling my mind with gaps. Even a connection to another gap is better than just a gap alone, at least then I am making progress.

[Johan Commelin]

I guess this depends a lot on the type of theory / conjecture you are talking about.

[Johan Commelin]

For many things, Wiki is great. But on the other end of the spectrum, there are conjectures, where you need to be in Bonn, or at MIT, or wherever, to start learning about them.

[Johan Commelin]

In general, I would say: check Wiki. If it isn't covered, do a quick internet search. If that doesn't show up anything on Encyclopedia of Math, or planetmath, or groupprops, or math.stackexchange, then you can ask a question on math.stackexchange.

If it is slightly Lean/mathlib related, just ask a question in #maths. The cool thing about this community is that you have access to a bunch of friendly experts that will be happy to give you a pointer, or a more detailed explanation.

[Julian Berman]

@Eric Taucher it's not directly related to your question perhaps, but I have in the back of my head that at some point I would like to try to write some posts somewhere for "Lean for the Inept Mathematician" (or some less self-deprecating name :P) -- where I try to learn some math thing by reading some Lean API and walking through that and the math involved. It'd sort of be the Lean equivalent of a really useful early Python resource, this thing called PyMOTW (module of the week). I'm in a similar boat, where I have vague notions of some primitive undergrad mathematical ideas but I think the exercise of filling in some of those mental gaps "interactively" along with lean (and a reader) might make for decent content. I mention this in case the idea seems interesting and you care to help motivate getting it started :)

[Eric Taucher]

Julian Berman said:

you care to help motivate getting it started :)

Possibly.
What would be expected on my part?

On another site for Prolog every several months a similar topic comes up and then if dies out after a few weeks. The problem is that these false starts have been collecting for years and at times find themselves as top search results which then just adds more confusion to those already confused as they are more templates with a few example pages then a complete set of documentation or series of exercises.

On the positive side I have made learning Lean my major project for now so it should be something I work with daily for the next several months or more.

[Julian Berman]

I don't know, this idea is still half baked :) -- but I think we'd need to brainstorm a first topic, some piece of math that is self contained enough to explain in 500-1000 words with like 3-5 pieces of Lean API related to it, and then stick some prose in a repo. To your point I think putting it anywhere indexable may not be wise until it turns out the idea sticks, so I was personally just planning to stick it in a git repo somewhere as soon as I got comfortable enough with Lean (has not happened yet but may never happen so may as well dive in at some point).

On the positive side I have made learning Lean my major project for now so it should be something I work with daily for the next several months or more.

Nice, lucky you.

[Eric Taucher]

Julian Berman said:

this idea is still half baked :)

I can live with that. Have to start somewhere.

brainstorm a first topic

My thought on this, since proofs generally form a DAG is to start as close to the bottom as possible, (Mizar graph) I know there is a similar image for Lean I just can find it at the moment.

some piece of math that is self contained enough to explain in 500-1000 words with like 3-5 pieces of Lean API related to it, and then stick some prose in a repo.

:+1:
Too much information scares new users.

To your point I think putting it anywhere indexable may not be wise until it turns out the idea sticks, so I was personally just planning to stick it in a git repo somewhere as soon as I got comfortable enough with Lean (has not happened yet but may never happen so may as well dive in at some point).

:+1:

[Arthur Paulino]

Lean for the Inept Mathematician? I'm in if you need another pair of hands :D

[Arthur Paulino]

Regarding sources for math theory, I found this yesterday, here on zulip:
https://stacks.math.columbia.edu/

[Arthur Paulino]

For a starting topic, I would probably suggest algebra

[Arthur Paulino]

Or maybe euclidean geometry if we can get TikZ working with lean comments somehow

[Eric Taucher]

Apparently this topic has serendipitously morphed into something better. Maybe we should split part of it off into a new topic or I can change the title so it gets more traction or is more meaningful when searching.

[Eric Taucher]

For Lean for the Inept Mathematician who would the target audience be? What expectations of math would be needed?

I did a very quick glance at https://stacks.math.columbia.edu/ and when ring was mentioned I knew the word and some of the concepts but could not have an intelligent conversation with some one with a math background.

[Arthur Paulino]

Eric Taucher said:

For Lean for the Inept Mathematician who would the target audience be? What expectations of math would be needed?

To make it easier, maybe the target audience could be ourselves (or some recent version of our past selves): people with enough experience in programming, who probably took CS classes, did calculus 1 or 2, linear algebra 1, basic discrete mathematics and had a short introduction to algebra and group theory, but nothing too deep (talking about myself here)

[Julian Berman]

I'm going to create a repo to start I suppose, maybe that removes some initial inertia. Audience-wise I was assuming a vague thing like "person interested in Lean who is not a mathematician" -- which means yeah you may kind of know what a ring is but probably wouldn't mind seeing someone remind you of the definition if the article was about the basics of ring theory (and if it wasn't, maybe it starts off by linking to some definition of a ring).

[Julian Berman]

Yes definitely "ourselves" is another good one!

[Arthur Paulino]

"person interested in Lean who is not a mathematician" or "person interested in mathematics and thought of Lean as a good interactive tool to learn it". Both are very similar profiles I think

[Arthur Paulino]

I thought of "ourselves" as a good target audience because it would be amazing to get to the point of actually being able to understand some of the talks that happen under #maths :smiley:

[Julian Berman]

OK repo is here: https://github.com/Julian/lftim -- if you (or anyone) wants commit rights just let me know your GH username

[Julian Berman]

Will set up github pages too perhaps

[Julian Berman]

Though maybe that creeps into "indexable" territory from above.

[Julian Berman]

But it will be easier to read if we put latex in a post or something.

[Arthur Paulino]

arthurpaulino :+1:

[Eric Taucher]

Personally I have no problem with Lean for the Inept Mathematician the definition of inept with regards to my knowledge of math and Lean here fits. That is not saying I don't have a knowledge of math or an understanding of Proof Systems, it is jus that the cross roads of the two greatly diminishes my connections to the ideas in context on this forum. That is not a fault of anyone but an opportunity for me to excel.

[Julian Berman]

Yes definitely agreed, to me the name seemed fitting as well :P

[Bryan Gin-ge Chen]

Some replies to this thread were split off to https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.20for.20the.20Inept.20Mathematician