ccn (new member)

Stream: new members

[ccn]

Hi there, I am just making an introductory post. I am a student at University of Toronto doing a computer science and mathematics major, is anyone else from there?

I maintain a wiki page where I store things that I have proven (usually typeset in latex), but I wanted to try out proving things with this.

I am completely new to how this works, but I was looking in the library itself and found this: image.png

I was wondering where I can read the proof for these theorems.

Also If I prove something in real life, on pen and paper, could I put it into the library? I guess what is acceptable to go in or not.

Thanks!

[Kevin Buzzard]

You can click on "source" on the right, and you'll see a bunch of code which Lean interprets as a proof.

[Kevin Buzzard]

I've proved a ton of stuff in real life, on pen and paper, and then put it into the library :-) But it took me a while to learn the language.

[ccn]

Oh that's exciting!

I just looked at the source

lemma exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum (hf : ∀ a ∈ s, f a ∈ t)
  (hb : t.card •ℕ b < ∑ x in s, w x) :
  ∃ y ∈ t, b < ∑ x in s.filter (λ x, f x = y), w x :=
exists_lt_of_sum_lt $ by simpa only [sum_fiberwise_of_maps_to hf, sum_const]

and to be honest I don't really know what's happening there yet haha.

[ccn]

Anyways, I'll do the tutorials, and see if I can eventually understand that

Just one last quesiton, I proved this a couple days ago, is this somthing that I could put into it? It's more like a question, but just wanted your opinion:

http://keepaskingwhy.com/mediawiki/index.php/How_many_times

What would this end up looking like in the language (just a description would be fine, would I be using other people's proofs inside of my proof? Or would it be from scratch?)

[Logan Murphy]

Welcome! I'm a CS grad student at UofT. Yury Kudryashov is also a Postdoc in Math at UofT, he is a very active contributor to mathlib.

[ccn]

Good to know!

[Logan Murphy]

I don't have anything to say about your proof you linked, but you should definitely try to work through as much of TPIL as you can (if you haven't done so). Some of the stuff in the lemma you posted is specific to mathlib (as opposed to core Lean), and beyond the scope of that book, but it will give you most of what you need to start exploring mathlib. It's definitely a learning process!

[Kevin Buzzard]

Mathlib tends not to have "random" recreational maths problems in. There are some International Maths Olympiad solutions in, but they're not in src where all the e.g. undergrad/MSc maths is. At the minute one of the main focuses is on theory-building, trying to get mathlib into a state where it can at least understand the statements of the main theorems in a generic pure math UG class.

[Kevin Buzzard]

On the other hand, people make random repos with their solutions to problems, so I could totally imagine you formalising this in Lean and putting it up on github as a repository which has mathlib as a dependency.

[Kevin Buzzard]

The kind of stuff I've done which has gone into mathlib has been stuff like the theorems I teach to undergraduates or MSc students.

[ccn]

That makes sense. Is there any interest in creating a more singular source for these "off-hand" type math problems. That one is actually useful because it's the number of iterations of a while loop of the form

while x > 0:
  x  = x//2

[ccn]

Oh yeah, another question, is it possible to generate a readable proof (like a proof you would see in a textbook, so it's readable who don't know lean) from a proof in lean?

[Kevin Buzzard]

I would imagine that every person who was interested in "off-hand" problems would be interested in different problems. There was quite a long debate about whether we should be putting IMO problems into mathlib, and currently they're there but in a directory of their own. These questions are complicated from a maintenance point of view. Mathlib is not backwards compatible and the maintainers can easily merge ten PR's in a day, some of which can break stuff. Feel free to make your own repo though, this is one way that people learn.

[Kevin Buzzard]

The easiest way to generate a readable proof is of course to learn the language and then you can just read the proof :-) Right now, the easiest way to make a proof human-readable is simply to write what you're doing in comments in your code. There are tools which can then e.g. turn it into a web page like this http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html or a game like this http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ .

[Kevin Buzzard]

For the sandwich theorem, if you click on a line in the proof you'll see the gobble-de-gook code, but then if you click on a grey rectangle you will be able to see the state Lean's brain at that point, which is often much easier to understand if you have a mathematical background.

[Kevin Buzzard]

By the way, I run a formalising club on Thursday evenings (i.e. right now, I'm in UK) on Discord where I teach undergraduates the language (and sometimes they teach me, indeed an UG and a PhD student are just showing me how to do a certain integral in Lean)

[ccn]

Kevin Buzzard said:

The easiest way to generate a readable proof is of course to learn the language and then you can just read the proof :-) Right now, the easiest way to make a proof human-readable is simply to write what you're doing in comments in your code. There are tools which can then e.g. turn it into a web page like this http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html or a game like this http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ .

That's super cool

[ccn]

Kevin Buzzard said:

By the way, I run a formalising club on Thursday evenings (i.e. right now, I'm in UK) on Discord where I teach undergraduates the language (and sometimes they teach me, indeed an UG and a PhD student are just showing me how to do a certain integral in Lean)

Can I join it?

[ccn]

(was all that text generated from the lean proof? )

[Logan Murphy]

I'm pretty sure those are basically just nicely formatted comments. No one has written a Lean-to-English machine (yet).

[ccn]

Oh I see

[Logan Murphy]

If you really want to show a particular Lean proof to non-Lean users, you can do some a pretty wide range of things by extending Lean's parser, so that things which Lean can interpret can be made to look pretty similar to something a mathematician can read.