math paper draft about proofs and lean

Stream: general

[SeniorMars]

Hello, I would like if someone could peer-review a paper i wrote about proofs and lean. I took great care in writing it so i would appreciate any advice on how to make it better.
main.pdf

[SeniorMars]

It's called: "A Critique Of The Mathematical Proof:
Formal Verification Of Partial Differential
Equations Through The Lean Theorem Prover"

[Eric Wieser]

Some initial feedback: it looks like you are having font issues with LaTeX, as many important characters are missing from your Lean code.

[Oliver Nash]

Thanks for writing this. I confess that I have only skimmed it but one thing that caught my eye were the remarks (section IV, top RHS of page 6) about desirability of formalising smooth partitions of unity, approximation theorems, regularization techniques. Are you aware that some of this material already exists?

See e.g., docs#SmoothPartitionOfUnity docs#HasCompactSupport.contDiff_convolution_left docs#ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints

[Oliver Nash]

In section V I think you're also overstating things somewhat. For example I can't quite agree with the claims:

However, analysis, which is crucial for the study of PDEs,
is notably underdeveloped. For instance, the concept of
partial derivatives, a fundamental tool in PDEs, is not
standardized in Lean.

[Oliver Nash]

I don't completely disagree (I even made some remarks in this direction myself recently https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Partial.20derivatives/near/467823912) I just think that you're overstating things. We do have plenty of analysis and we have a very well-developed theory of multidimensional calculus: it's just not done in the way this stuff is often taught.

[Bhavik Mehta]

Early in Section III you write

Moreover, one of Lean’s most notable features is its emphasis on constructive mathematics. While it supports classical reasoning through the inclusion of the law of excluded middle as an axiom, Lean encourages users to provide constructive proofs whenever possible.

I don't think this assessment aligns with many users' experiences, and almost every analysis proof using Mathlib will be non-constructive. I would argue that Mathlib strongly encourages users to provide non-constructive proofs (sometimes even when constructive proofs are available!)

[Ruben Van de Velde]

While lean makes it possible, mathlib very much isn't interested

[Eric Wieser]

Ruben Van de Velde said:

While lean makes it possible, mathlib very much isn't interested

I think while Lean makes it possible, it is also not at all interested, as many core tactics use classical logic and PRs to change this were rejected.

[Eric Wieser]

Though if enough people appeared and said "I want to do constructive logic in Lean", that might change

[SeniorMars]

thank you so much for this feedback!

[SeniorMars]

@Bhavik Mehta I have used lean as a programming language more than mathlib, so thank you for bringing this up!

[SeniorMars]

Oliver Nash said:

In section V I think you're also overstating things somewhat. For example I can't quite agree with the claims:

However, analysis, which is crucial for the study of PDEs,
is notably underdeveloped. For instance, the concept of
partial derivatives, a fundamental tool in PDEs, is not
standardized in Lean.

You make an excellent point that I never thought of! I will def expand on this.

[Patrick Massot]

Eric Wieser said:

Though if enough people appeared and said "I want to do constructive logic in Lean", that might change

I don’t think this would be sufficient. You would need some people appearing and saying: “I want to do something impactful using constructive logic in Lean”.

[Edward van de Meent]

you're saying there is no amount of people that would be enough??

[Jireh Loreaux]

Patrick Massot said:

Eric Wieser said:

Though if enough people appeared and said "I want to do constructive logic in Lean", that might change

I don’t think this would be sufficient. You would need some people appearing and saying: “I want to do something impactful using constructive logic in Lean”.

Even more is necessary: "... and it's not possible to do it effectively / efficiently with classical reasoning."

[Mario Carneiro]

I wonder whether any interesting applications will come up in the upcoming agda implementers meeting

[Martin Dvořák]

Nicely written article! I enjoyed reading it!

PM me if you need help with the visibility of special symbols.

[Kevin Buzzard]

Edward van de Meent said:

you're saying there is no amount of people that would be enough??

The conclusion of the debate about constructive logic was something like: the FRO did not have the resources to start changing core features to accommodate people who wanted to use Lean constructively, and that this was unlikely to change unless (and this was the FRO's words) "impactful" projects which need constructive logic were proposed. Examples of impactful projects using classical logic were some of the recent high-profile mathematics projects (getting featured in Nature, Quanta etc). So yes, it's not about people: constructivists are not hard to find, you can find them in the theory groups in many computer science departments. My impression is that many of them cannot use Lean for lots of reasons, not just the fact that some core tactics use classical logic. For example the univalence axiom is false in Lean, and this is very unlikely to change any time soon.

[Bulhwi Cha]

There are already various proof assistants, so I think it'd be better for constructivists to explore those other than Lean.

[Mario Carneiro]

I kind of want to suggest making a lean fork with a super-hackable kernel as an alternative to "Agda 2" for resolving tech debt issues in the agda community at the implementers meeting. I strongly suspect that the architecture of lean is actually very well suited to type theory playground stuff, and it wouldn't be hard to open up the kernel while keeping the other niceties of the elaborator. (But I think it would be best to position such a project as something entirely separate from lean as an organizational body.)