Lean for Thermodynamical Proofs

Stream: lean4

[Heime]

I want to specify a thermodynamic system and need help to set it up.

[Henrik Böving]

Given that you have just installed Lean, have you done any Lean before at all?

[Heime]

Of course not.

[Heime]

I done lot of software design before.

[Henrik Böving]

Lean is not software design, if you don't have experience with teh basics of Lean helping you set up whatever is pretty pointless

[Heime]

Are there any completed proofs from signal analysis in Lean that I can look and learn from ? Integral transforms (fourier, wavelets) or from sequence and series convergence ?

[Heime]

Delved into Coq but found it terribly long to gets to follow an actual non-trivial proof without spending weeks focused on Coq Structures.

[Heime]

Is Lean any better ?

[Eric Wieser]

Maybe something like this slide and the ones around it are interesting to you, if you want a high level view of what some mathematics in similar areas looks like in Lean? Those slides are about lean 3, but you should be able to search for the corresponding lean4 results in the #docs.

[Heime]

If I search the lean4 results in the docs are these definitions (coding in Lean) or actually proving something with lean. I want to prove things in Lean. Not learning to code in Lean.

[Eric Wieser]

I don't really understand the distinction you are trying to draw

[Eric Wieser]

docs#tsum_sq_fourierCoeff is the lemma in question there

[Eric Wieser]

If you want to "follow" the proof, you will need to get your installation working first though; lean proofs are mostly written on the assumption that you are reading them with a working lean install and a clever editor of your choice.

[Heime]

Aren't there any books and tutorials showing how proofs are verified ? I am looking for simple undergraduate theorems that have already been proved, to see how it is done.

[Shreyas Srinivas]

There are a few different books for basic theorem proving in lean, starting with #tpil
There are games like #nng4 and the set theory game to learn the basic tactics.

That being said, without familiarity with lean the programming language, the metaprogramming facilities will prove hard to get started on.

[Shreyas Srinivas]

Also, for your specified interests, I suggest taking a look at scilean and the natural sciences stream on this zulip. There are a few discussions you might find informative

[Heime]

Regarding docs#tsum_sq_fourierCoeff

Is that a statement of the theorem, or its proof ?

[Shreyas Srinivas]

What's listed there is a statement. You can click on the source link of the panel to see the tactic proof

[Shreyas Srinivas]

But in order to understand what that proof is doing, it is best to clone mathlib, set it up as per the README, and interact with it on vscode

[Shreyas Srinivas]

(deleted)

[Heime]

Right. Rather than the statement of the theorems, I am more interested to see the actual proof that gets verified by lean.

[Shreyas Srinivas]

Then you need to click on the source link of the panel. What you see is a tactic script that generates the proof

[Heime]

Is there anything about convergence of sequences and series. Have been looking, but cannot find anything yet.

[Shreyas Srinivas]

I doubt that you'll find proofs of convergence of specific series. It is more likely that there are general theorems of convergence. You could search moogle or loogle. Moogle supports natural language queries whereas loogle is a lot like Haskell's hoogle, which looks for specific patterns

[Shreyas Srinivas]

If you wish to learn proving things like that, you could check out the #mil book (Mathematics in lean)

[Kim Morrison]

src#Real.tendsto_sum_range_one_div_nat_succ_atTop is the divergence of the harmonic series, as an example.

[Kim Morrison]

Echoing the suggestion to read #mil, but if you give some concrete examples people will probably be happy to help.

[Heime]

It is a shame that the book is not in pdf as well. At any rate, I shall go through it to see how much it would help me.

[Heime]

But I can see that making sense of the proofs is hard. Very hard actually !

[Shreyas Srinivas]

You can get the pdf from its github repository : https://github.com/leanprover-community/mathematics_in_lean/blob/master/mathematics_in_lean.pdf

[Shreyas Srinivas]

Heime said:

But I can see that making sense of the proofs is hard. Very hard actually !

What you see as "proofs" in lean are scripts composed of tactics. Tactics are metaprograms that construct and supply a proof term in pieces. The proof terms produced by tactics can be rather unwieldy. A better way to understand them is to work with them through examples. This is where games come in handy : https://adam.math.hhu.de/

[Heime]

Fantastic discovery. There are two things to get used to: 1) Formalising mathematics for lean and 2) Proving the statements.

[Heime]

What basic and useful tactics should I learn about as I start with all this ?

[Shreyas Srinivas]

I recommend following the natural number game. The tactics you need largely depend on what you do with lean, but that game has the basics. An almost certaintly incomplete common baseline could be : rfl, rw, exact (and exact?), apply(and apply?), intro, use, revert, cases, induction, gcongr, have/replace,induction, and simp.

[Shreyas Srinivas]

But there's a lot more than these and many ways to combine them.

[Heime]

Is there also a pdf for "Theorem Proving in Lean 4" ?

[Shreyas Srinivas]

It's an mdbook. On the top right corner, next to the github icon you should be able to see a printer icon which you you can use to save the book as a pdf.

[Shreyas Srinivas]

You might find this tactic cheatsheet by @Martin Dvořák useful : https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

[Heime]

Have found the printer icon as you say. Thank you so very much for the cheat sheet. I am generally in contrasting mood to mathematicians as I often want to go through things fast.

[Martin Dvořák]

Shreyas Srinivas said:

You might find this tactic cheatsheet by Martin Dvořák useful : https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

That one is for print and is a bit obsolete. If you want to read it on your computer, I recommend this one:
https://github.com/madvorak/lean4-tactics

[Ralf Stephan]

As another newcomer from the software side, I strongly advise you not to read PDFs but actually run any code you see in a Lean-enabled editor, in order to see the state of the proof after each operation. Otherwise you won't be able to follow the steep learning curve, at all, that lies ahead of you.

[Heime]

How can we solve this disease that whatever is done, it is done hard !

[Eric Wieser]

Well, it sounds like you're the one asking for the "hard" PDF copy of the documentation, rather than using the web version :upside_down:. What exactly do you mean by that?

[Eric Wieser]

I don't think it's remotely fair to the developers or the community to describe any part of Lean as a "disease", except for the fact that wanting to prove in it seems contagious!

[Heime]

The steep learning curve is a reality. To look at things the way they are is something that many are not comfortable with. Have realised that humans have not evolved as much as we think we have. If this will be the future of mathematics, there will be very few.

[Johan Commelin]

@Heime Please come with concrete suggestions for improvement instead of unconstructively labelling things "disease" or not "decent" etc...

[Bulhwi Cha]

Heime said:

To look at things the way they are is something that many are not comfortable with.

I've met some Koreans who complained that formalized mathematics doesn't "look like" standard mathematics. I agree that we need a new method for writing formal proofs other than tactics or proof terms. I hope it'll resemble writing Fitch-style proofs.

However, I think tactic proofs are better in some cases. For example, I spent about 170 hours proving the theorem String.splitOn_of_valid. See std#743. Tactics make it much easier to simplify proof goals. I can't imagine writing an informal proof of this theorem without referring to the formal proof written in Lean.

Besides, even I don't want to have an in-depth understanding of the proof I wrote. It's too complicated. In this case, tactic proofs are just fine because you only want to confirm that the proof is correct. Would an informal proof of String.splitOn_of_valid be much easier to understand? Probably yes, but only when it omitted many proof steps requiring delicacy.

Heime said:

How can we solve this disease that whatever is done, it is done hard !

In conclusion, that "disease" saved my time. There's a good reason to do something the hard way.

[Johan Commelin]

But Fitch-style proofs don't look like standard mathematics either!

[Bulhwi Cha]

Johan Commelin said:

But Fitch-style proofs don't look like standard mathematics either!

Um, that's why I think the Koreans I mentioned wouldn't like Fitch-style proofs either. However, these proofs have the advantage of not requiring a user to run a proof assistant to examine the proof state of each step.

[Bulhwi Cha]

I still don't know what the new method for writing formal proofs would exactly look like. I need to study more.

[Utensil Song]

#explode gives a Fitch-style proof that's very helpful for figuring out what happened during the tactics and a possible better path. It seems easier to convert to informal proofs from there while maybe losing high-level ideas expressed by high-level tactics with a semantic similar to informal proofs.

[Bulhwi Cha]

The result of running #explode String.lt_iff_toList_lt is in https://paste.sr.ht/~chabulhwi/c57c0555c142cbd2eaf1ee4401fd3b94c764acca.

My goal is to make auto-generated Fitch-style proofs more readable.

[Mario Carneiro]

I think there was a version of explode that generated HTML instead of ASCII art, which is a bit easier to keep aligned when there are long subexpressions

[Mario Carneiro]

The original #explode predates infoview widgets, but I think we can do a lot better these days presentation-wise

[Eric Wieser]

There is some code at https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Tactic/ExplodeWidget.lean that could be adapted

[Bulhwi Cha]

I also want to have the option to hide the inner workings of tactics when using the #explode command. I'll try to make it in the future.