mathematical insights from formalization

Stream: general

[Jeremy Avigad]

On Wednesday, I'll be giving a talk in a Mathematical Components workshop (https://mathcomp-schools.gitlabpages.inria.fr/2022-12-school/). I expect that many of the participants will be from the computer science community, and since there have historically been tensions between the mathematical and computer science communities over formalization, I'd like to take the opportunity to say something about how mathematicians think differently from computer scientists.

One difference I have noticed is that when computer scientists review a formalization paper, they expect to hear a lot about the encodings, representations, and formalization tricks that were used -- the "design decisions." Mathematicians tend to focus instead on the mathematical insights when they write papers about formalization. To computer scientists, that often looks like they are just repeating standard and well-known mathematical definitions and theorems.

I'd like to give a list of examples of mathematical insights that have come out of formalization, or, least, formalization insights that have more of a mathematical flavor than a computer science one. Below is the list I came up with. I am curious to hear what others think of the list, and what they might add.

• Filters are the right way to deal with topological limits.
• The Bochner integral and the Frechet derivative are just the right level of generality.
• Uniform spaces are useful (generalizing both metric spaces and topological groups).
• Embeddings and homomorphic images often work better than subsets and substructures.
• There are lots of ways of formalizing the notion of a sheaf. Some work better than others.
• If K is a field extension of F, it is often better to treat K as an F-algebra (especially with towers of extensions).
• It's possible to unify real and complex inner product spaces with the right type class.
• Semilinear maps are a useful generalization of linear maps and conjugate linear maps.
• Manifolds with corners are better than manifolds with boundary.

Note that I am not claiming that these originated with Lean. Filters were used by Hölzl, Immler, and Huffmann in Isabelle, and also by Beeson and Wiedijk in the context of a algebra system; the idea goes back to Bourbaki. In Lean, we also took the Bochner integral and the Frechet derivative from Isabelle, as well as the is_R_or_C type class.

[Eric Rodriguez]

The Commelin complex? Although iirc that was found to have alredy been discovered before

[Yakov Pechersky]

Meta-formalization: how about the impact of CI/CD for communication of results, both internal and external? This topic, in my mind, rhymes with the impact of LaTeX.

[Jeremy Avigad]

I will also talk about LTE, and quote Scholze on an insight he had from the formalization. And I will also say a lot about the controlled chaos of the Lean community and how well it works.

[Riccardo Brasca]

I would remove

• If K is a field extension of F, it is often better to treat K as an F-algebra (especially with towers of extensions)

This is surely true, but it has nothing to do with formalization, it's just something we all know, even if often we write proofs at the blackboard like F is a subset of K (for example I've discussed how to do this in teaching before having heard abut Lean). It's like the fact that ℕ is not a subset of ℤ, we know it, and when Lean recalls it to us it's only annoying, not useful.

[Jeremy Avigad]

IIRC @Heather Macbeth has been working with others on cleaning up something involving manifolds or differential geometry or something like that -- does anyone know the details?

[Mario Carneiro]

Riccardo Brasca said:

I would remove

• If K is a field extension of F, it is often better to treat K as an F-algebra (especially with towers of extensions)

This is surely true, but it has nothing to do with formalization, it's just something we all know, even if often we write proofs at the blackboard like F is a subset of K (for example I've discussed how to do this in teaching before having heard abut Lean). It's like the fact that ℕ is not a subset of ℤ, we know it, and when Lean recalls it to us it's only annoying, not useful.

I disagree with this. It is very much not obvious to what degree you can take seriously the assertion that field extensions are always subset relations and work everything into that framework. It clearly works for paper mathematics, so why not in the computer? For systems like lean where literal subsetting isn't really an option it doesn't matter that much, but if you are working in a ZFC based system it is a very real possibility to do things in this way.

[Jeremy Avigad]

Riccardo, a long time ago I saw Kevin Buzzard give a talk about the difficulties of mediating between Q[sqrt2][sqrt3] and Q[sqrt 3][sqrt 2] and Q[sqrt 2, sqrt 3]. My understanding is that it took Baanen and others some experimentation to come up with a nice way of doing class field theory. Most of the examples I listed involve things that are well known from a mathematical standpoint. The insights are that they are a good way of organizing and presenting the material, especially from the point of view of formalization.

[Riccardo Brasca]

Maybe I was not clear: I am not saying extensions should be considered as inclusions, but quite the opposite.

The difference with, say, filters is that we're able to talk about limits without using filters, and formalization force us to have a more general notion. I don't think anyone has seriously tried to study field theory using inclusions.

[Mario Carneiro]

No I understood that. What I'm saying is that extensions as inclusions is a very obvious thing if you look at the way paper mathematics is done, and it is a hard won lesson to discover that it's not a good idea.

[Riccardo Brasca]

Mario Carneiro said:

Riccardo Brasca said:

I would remove

• If K is a field extension of F, it is often better to treat K as an F-algebra (especially with towers of extensions)

This is surely true, but it has nothing to do with formalization, it's just something we all know, even if often we write proofs at the blackboard like F is a subset of K (for example I've discussed how to do this in teaching before having heard abut Lean). It's like the fact that ℕ is not a subset of ℤ, we know it, and when Lean recalls it to us it's only annoying, not useful.

I disagree with this. It is very much not obvious to what degree you can take seriously the assertion that field extensions are always subset relations and work everything into that framework. It clearly works for paper mathematics, so why not in the computer? For systems like lean where literal subsetting isn't really an option it doesn't matter that much, but if you are working in a ZFC based system it is a very real possibility to do things in this way.

I don't think "it clearly works on paper". It works because we are good in filling the holes when reading mathematics. If Lean were able to do the same, then I would say this is a good thing

[Mario Carneiro]

It definitely works on paper. Every field extension is isomorphic to a subset, so everything transfers and you're done

[Riccardo Brasca]

Sure, it's the "everything transfers" part that we are very good in doing. In any case I agree that in Lean it would be much more painful to transfer everything.

[Mario Carneiro]

but you don't know to focus on that part of the claim unless you have some formalization experience under your belt already

[Mario Carneiro]

this "do what I mean, not what I say" business is very tricky for formalizers who aren't experts already

[Adam Topaz]

Here is a quick personal story (and a shameless plug): A little while ago I formalized the proof of a somewhat technical result from my area of research here: https://github.com/adamtopaz/lean-acl-pairs
The primary goal of this formalization was to prove the result in the following file:
https://github.com/adamtopaz/lean-acl-pairs/blob/master/src/main_theorem.lean
The proof was based on an argument I wrote down in an earlier paper which was very explicit (and hence amenable to formalization).
Already when I wrote that explicit argument I realized that there was something new that could be done in another context, and it was a complete triviality to formalize this new theorem based on the other parts that were already formalized.
The new theorem is formalized here: https://github.com/adamtopaz/lean-acl-pairs/blob/master/src/main_theorem_char.lean
and I even wrote a tiny paper about this "new" result here: https://raw.githubusercontent.com/adamtopaz/CoeffAltPairs/main/main.pdf

It's not quite correct to say that the formalization was the catalyst needed for this new theorem, but rather the proof that was formalizable made it possible.

[Jeremy Avigad]

Adam, that's a good story. I will likely repeat it to others, if you don't mind.

[Adam Topaz]

Another mini-example: Over the summer of 2022, @Jack McKoen and I formalized some results about valuation rings (which made it to mathlib). We then started thinking about formalizing a theorem called "the approximation theorem for independent valuations" which involves some understanding of the topology on fields induced by valuations. In true mathlib fashion, we started with arbitrary rings as opposed to fields, and realized that something nontrivial could indeed be done in this more general context (this also involves some compatibility with uniform structures on rings). I haven't seen any such results in the literature, especially not anything that relates such topologies on rings to uniform structures. So in this case, I would say that the formalization process (or rather the natural boundaries suggested/enforced by mathlib) did indeed contribute to some genuinely new mathematical insight (even though this new mathematics is still "work in progress").

[Adam Topaz]

@Jeremy Avigad sure, I don't mind!

[Patrick Massot]

Jeremy Avigad said:

I'd like to give a list of examples of mathematical insights that have come out of formalization, or, least, formalization insights that have more of a mathematical flavor than a computer science one. Below is the list I came up with. I am curious to hear what others think of the list, and what they might add.

You need to be really careful about this because for almost any example people will tell you this was already known and has nothing to do with formalization.

• Filters are the right way to deal with topological limits.

It's a lot more than this in mathlib.

• The Bochner integral and the Frechet derivative are just the right level of generality.

For Frechet derivative this is clear to anyone working in pure math. I learned about Bochner integration in mathlib, but clearly a lot of people know about it.

• Uniform spaces are useful (generalizing both metric spaces and topological groups).

Of course Bourbaki knew this in the 40s but I think it's safe to say that the average mathematician has never heard of uniform spaces.

• Embeddings and homomorphic images often work better than subsets and substructures.

Again this is will known, especially from a categorical point of view, but indeed you need to take it much more seriously when formalizing.

• There are lots of ways of formalizing the notion of a sheaf. Some work better than others.

This is really vague.

• If K is a field extension of F, it is often better to treat K as an F-algebra (especially with towers of extensions).

Again, this is well known but indeed you need to take it much more seriously when formalizing. And I disagree with Mario that seing all extensions as subset is viable on paper.

• It's possible to unify real and complex inner product spaces with the right type class.

Here you can easily claim that people think it should be doable on paper but it's never done.

• Semilinear maps are a useful generalization of linear maps and conjugate linear maps.

Said like this people will think it's well known. The very nice work of Heather, Rob and Frédéric is really about making this doable in Lean.

• Manifolds with corners are better than manifolds with boundary.

Again, this is well known but indeed you need to take it much more seriously when formalizing.

[Patrick Massot]

One thing that I think is typical of using a proof assistant is using more "induction principle". For instance on paper we would never state docs#is_compact.induction_on or exists_cont_mdiff_of_convex. There are also nice examples in the Galois theory paper.

[Kevin Buzzard]

Regarding the idea that a field extension K/F is an F-algebra I agree with Jeremy and I still remember the time when we were stuck on this. People who want to see me whingeing can search for the old algebra is not scaling for me thread in #maths. If you want to do basic stuff about ring or field extensions K/F then you can choose: either F is a type (so K is an F-algebra) or F is a term (F is a subring of K). Mathematically these are both the same, and you can develop the theory in either setting. When things get interesting is when you're formalising MSc level commutative algebra and you have rings $A\subset B \subset C$ and some technical statement like the Artin-Tate lemma whose proof involves constructing a sub-A-algebra B_0 of B. It's at this point you realise that your design decisions now really matter. You want C to be an A-module and B to be a subring of C and B to be an A-algebra etc etc all at the same time and you can't have all of these things at the same time. Riccardo you're wrong when you say that nobody tried to study field theory using inclusions. Me and Kenny were thinking about this a lot in 2018-19 and at that time we were really stuck about how to make everything work at once. In the Coq odd order paper they make everything a term! They have a big universal group and all groups are subgroups of this group. This worked great for them but it doesn't work in ring theory because given two groups you can always find a bigger group containing both of them (namely the direct product) but the same is not true for rings ($A$ is not a subring of $A\times B$ because the 1s don't match). For homogeneity reasons the next solution to try is making everything a type but here you have problems because you want too many things to be algebras over too many other things all at the same time. Then Kenny invented algebra_tower and all of a sudden we were back on track. Then Eric came along and invented is_scalar_tower and now today here we all are thinking that MSc level commutative algebra is easy because we've forgotten the pain of 2018 when we were still very unsure about whether algebra or subring was the best approach and both of them had problems.

[Jeremy Avigad]

Thanks, Patrick. The last comment is very helpful.

I'll try to make it clear that I am not claiming that these insights are new mathematics. Rather, I want to say that we are learning something about how to organize mathematics to make it formalizable.

[tica]

(deleted)

[Kevin Buzzard]

@tica you're in the wrong thread; this is a discussion about mathematical insights from formalisation. Can you please start a new thread perhaps in #maths ?

[Kevin Buzzard]

Regarding Patrick's comments -- it's almost certainly true that if it's at undergraduate level then it's been tried before, because I would imagine everything has been tried before. No doubt formalising topology using open sets has been tried before, no doubt the Riemann integral has been tried before, no doubt semilinear maps have been tried before. It's not about the definition having been tried before. It's about a fundamental definition having a huge amount of material being built on top of it and seeing if it withstands the strain.

Having said that, it might be the case that mathematicians are simply not particularly interested in these design decisions, so they choose not to stress them. For example Oliver had to make a bunch of design decisions in his Lie algebra paper but as a mathematician his instinct is to actually devote most of his time talking about how he's found a new and more conceptual way of thinking about Engel's theorem, because to people like him and me this abstraction is kind of cute and interesting, whereas talking about non-associative algebras is just some foundational thing that "we all know now that we can do in Lean" because Lean has already proved its worth when it comes to formalising mathematics.

[Riccardo Brasca]

The very fact that we're having this discussion is probably a proof that formalization can teach something about field extensions, but I am a little bit surprised: of course very often I think like the smaller field is a subset of the big one, but if I ad to write an algebra book I have the impression that I would have defined things using algebras, even before having heard about formalization. Just because there is no way K is a subset of K[x]/p. I really feel like the situation for ℕ and ℤ: do you think formalization makes more clear wrt paper math that there is only a "canonical" map, rather than a real inclusion?

[Jeremy Avigad]

With this slide in my talk (which has now grown to two slides), I only want to make the case that these are insights worth documenting at least to the formalization community. The tendency I want to counter is to discount the value of a paper because it is "just a repeat of the mathematics" and doesn't spend enough time "describing the formalization."

The question as to the mathematical value of these insights, and as to the mathematical value of formalization in general, is a much bigger one. Johan made a great case for formalization in his Fields Medal Symposium talk. Here I am taking on the simpler task of trying to communicate to formalizers from a CS background what formalizers from a math background tend to find interesting and useful.

[Kevin Buzzard]

Another example of an implementation issue is the way complexes of objects in an abelian category are dealt with in LTE. Because we have this problem about A(n+1-1) and A(n) not being defeq if n is an int we tried several implementations and eventually decided on having maps A(i) -> A(j) for all i and j. I think Floris tried something else in his thesis but that was in a univalent setting which didn't have the problems we have in vanilla DTT. Paulson claims that the same problems would not exist in simple type theory.

[Kevin Buzzard]

Riccardo regarding the "obvious" idea that everything needs to be a type -- the problem with that is that you can't make C and B both A-algebras and C a B-algebra all at the same time until you have the idea of the implementation of is_scalar_tower, something which still looks totally counterintuitive to me -- it's a statement about heterogeneous associativity and it took a while to be discovered.

[Riccardo Brasca]

I am not saying it's easy to implement this in a formal language, I just mean that the situation in pen and paper math is pretty clear, a field extension is a ring hom K → L.

[Adam Topaz]

Just my 2c: In my opinion, one of the main points of Galois theory is to view a field extension as a morphism of fields and not just an inclusion!

[Kevin Buzzard]

I totally agree with all of this however none of this means that the best way to do it in lean is with types. I'm sure you'd also agree that one of the main points of complexes is that you have maps from A(n) to A(n+1) and that's not what we're doing.

[Adam Topaz]

Personally I feel that the trick we have with complexes with d i j going from A_i to A_j with i,j arbitrary (with some other axioms) is very far from the end of the story. Sure, it works (and LTE is good evidence that it works well enough), but I still don't think it's close to the optimal approach.

[Eric Wieser]

Kevin Buzzard said:

Then Eric came along and invented is_scalar_tower and now today here we all are thinking that MSc level commutative algebra is easy

Do you mean @Eric Rodriguez ? I certainly pushed for it to be used everywhere, but I can't take credit for it

[Moritz Doll]

I think that the Bochner integral is good is well-known to most people working in functional analysis/spectral theory. About the Fréchet derivative I think this is not as clear as you state it since there are areas of math that need Fréchet space valued derivatives.
As for the manifolds with corners, this is also very well-known in certain analysis communities (some of my research is about analysis on manifolds with corners), the simple reason is that if you want to analyze differential operators on $X$, then you are usually looking at the Schwartz kernel, which is a function on $X \times X$, which is a proper manifold with corners if $X$ is a manifold with boundary.

[Kevin Buzzard]

I think another issue is the following: this thread is full of people going "of course you do Galois theory like this, of course you do integrals like this, of course you do manifolds like this" but the point is that we are professional mathematicians and this is what was missing from the story. Before 2017 you could count the number of professional mathematicians in this area on the fingers of one hand.

By the way In one of Lang's books (Algebra?) he does Galois theory by replacing all field extensions K -> L with subfields K subset L' with L' defined to be the disjoint union of K and the things in L but not the image of K. Hindsight is a wonderful thing.

[Anne Baanen]

Eric Wieser said:

Kevin Buzzard said:

Then Eric came along and invented is_scalar_tower and now today here we all are thinking that MSc level commutative algebra is easy

Do you mean Eric Rodriguez ? I certainly pushed for it to be used everywhere, but I can't take credit for it

As far as I remember and can tell from Zulip and Git history, Kenny wrote the first implementation of is_algebra_tower (#3272) based on some of Johan's suggestions, which ultimately derive from Markus' diagram chasing tactic. AFAICT implementing it as a class is Kenny's innovation. Our current is_scalar_tower class was a slight modification done by me (#3717, #3785) based on my own experience and Kenny's recommendations. Certainly Eric Wieser should be remembered for spending a lot of effort trying to popularize its usage.

[Eric Wieser]

Oh this explains where the "algebra tower" terminology comes from in various docstrings / filenames, despite the fact that everything is now much more general than that. Thanks for the archaeology!

[Kevin Buzzard]

Sorry @Anne Baanen ! I seem to have misattributed the insight. Yes, it used to be called algebra_tower and only worked for rings

[Tyler Josephson ⚛️]

Though science and engineering applications sound like they might be outside the scope of what you’re speaking about, we’ve found the following neat benefit of formalization.

We wrote down proofs that the kinematic equations follow from the calculus-based definitions of the equations of motion (https://arxiv.org/abs/2210.12150). First year undergrads in Physics do these derivations with pencil and paper. But after we formalized them, @Max Bobbin realized that our proof need not assume that time was real - we could try more general types. Just go to the front of the proof, change time’s type to be the complex numbers, and most of the proofs still closed.

[Pedro Sánchez Terraf]

Jeremy Avigad said:

I'd like to give a list of examples of mathematical insights that have come out of formalization, or, least, formalization insights that have more of a mathematical flavor than a computer science one. Below is the list I came up with. I am curious to hear what others think of the list, and what they might add.

A bit of a truism because of its generality, but that might resonate with CS people, is that working in any formal system restricts the way things can be proved, like in the case of constructive approaches they are very fond of (avoiding EM, AC).

In the spirit of formalization (but actually a little of a reversal, like the beginning of one of Adam's examples) I wrote detailed proofs of the basic theory of cofinality of ordinals that confined induction/recursion to a single application in one lemma. I later formalized that proof, and that was convenient since I was working in Isabelle/ZF, where handling well-founded recursion was inconvenient.

The takeaway is that formalization may always inspire looking for the key lemma.

[Jeremy Avigad]

Many thanks to everyone for this feedback. Among other things, it got me to realize that initially I was somewhat confusedly asking two separate questions at once: (1) What are the insights from formalization that are of interest to mathematicians who formalize mathematics? (2) What are the insights from formalization that might be of broader mathematical interest?

Maybe there isn't a sharp line between the two questions, but this discussion has provided responses to both. It is helpful for thinking about how to communicate our work to others.

[Jeremy Avigad]

I guess I'll also add the thought that the reason that there isn't a sharp line between the two questions is that there isn't a sharp line between discovery and exposition, i.e. between coming up with new mathematical ideas and figuring out how to organize the knowledge we have and make it precise. Both are part of mathematics.

Mathematicians will bristle at the claim that is_scalar_tower is a real mathematical discovery, on the grounds that it is trivial and implicit in what they have been doing all along. We need to recognize this, but also emphasize the importance of finding the right ways to make our intuitions precise.

[Floris van Doorn]

One example I encountered (that is also a shameless plug) comes from formalizing the convolution of two functions (https://arxiv.org/abs/2210.07693, pp 10-11).
You want your definition of convolution to be able to express the smoothening of a multivariate function $f : \mathbb{R}^n \to \mathbb{R}^m$ using some bump function $\varphi : \mathbb{R}^n \to \mathbb{R}$. In this case, the convolution is defined to be $(\varphi*f)(x)=\int \varphi(t)f(x-t)dt$ (with scalar multiplication inside the integral).

We can then compute partial derivatives of such a convolution. Under appropriate conditions on $\varphi$ and $f$ we can compute e.g.
$\frac{\partial}{\partial x_i}(\varphi*f)= \frac{\partial\varphi}{\partial x_i}*f$.
It would also be nice to have a formula for the total derivative of $\varphi*f$. We would like to write that
$D(\varphi*f)=D\varphi*f$
except that the right-hand side doesn't type-check: how do we even define the convolution of $D\varphi$ and $f$? Neither of them is scalar-valued, so we cannot multiply the function values $D\varphi(t)$ and $f(x-t)$.

This is why the mathlib definition of docs#convolution takes two vector-valued functions $\varphi: G \to E$ and $f : G \to E'$ and a (continuous) bilinear map $L : E \to E' \to F$ to "multiply" the values (here $E$ and $E'$ are normed spaces, and $F$ is a Banach space). Then the definition of convolution is
$(\varphi*_Lf)(x)=\int_t L(\varphi(t),f(x-t))dt$
and we can then compute (under suitable hypotheses)
$D(\varphi*_Lf)=D\varphi*_{L'}f$
where $L'$ is defined by $L'(A,x,v)=L(Av,x)$.
(src#has_compact_support.has_fderiv_at_convolution_left)

[Floris van Doorn]

I have not seen any textbook use this approach. All the ones I consulted (with @Patrick Massot) only compute partial derivatives, and avoid writing the total derivative.

[Jeremy Avigad]

Nice!

[Filippo A. E. Nuccio]

Another example that I like very much comes from @Heather Macbeth 's work on the sphere as manifold. From the paper&pencil perspective, the "easiest" thing to do is to only fix two charts, one around the North Pole and one around the South, and then check that everything glues. Her insight is that fixing charts at every point of the sphere actually works better: it makes everything more natural (no poles any more :penguin: means no choice), adds very little burden — or no burden at all — to the theory, but it is not the usual way things are presented. Her slides here are very clear.

[Heather Macbeth]

In fact I got this idea from a comment of @Patrick Massot about projective space.

[Nilesh]

Tyler Josephson ⚛️ said:

First year undergrads in Physics do these derivations with pencil and paper. But after we formalized them, Max Bobbin realized that our proof need not assume that time was real - we could try more general types. Just go to the front of the proof, change time’s type to be the complex numbers, and most of the proofs still closed.

Oh, this is very interesting. Has someone attempted to formalize high-school or undergraduate physics? Laws of motion, gravitation, electromagnetism etc?

[Tyler Josephson ⚛️]

@Nilesh I’ve only found isolated projects, like refs 20 and 21 in our manuscript. But I’m working on laying the groundwork to start a Xena project-like program to teach UG’s how to formalize science and engineering theories, and build a “SciLib” database like mathlib.

[Jireh Loreaux]

FYI: @Tomas Skrivan has a project called SciLean, but I think it's more geared toward scientific computation rather than "science and engineering theories", but I could be wrong.

[Tyler Josephson ⚛️]

@Jireh Loreaux @Tomas Skrivan These go hand-in-hand! We can formally prove theories, and we can write scientific computing software that rigorously corresponds to said theories. I’d love to write statistical mechanics proofs, and then write SciLean software for molecular dynamics that provably simulates the canonical ensemble, for example.

[Sina]

Tyler Josephson ⚛️ said:

Jireh Loreaux Tomas Skrivan These go hand-in-hand! We can formally prove theories, and we can write scientific computing software that rigorously corresponds to said theories. I’d love to write statistical mechanics proofs, and then write SciLean software for molecular dynamics that provably simulates the canonical ensemble, for example.

Is there a tutorial on installing and using SciLean? How has been your experience with it?

[Tyler Josephson ⚛️]

We haven’t used it directly yet, but you can ask @Tomas Skrivan any questions you may have!

[Tomas Skrivan]

I wrote few things here. Unfortunately, the library is not practically usable yet and still in heavy development. Some core pieces will have to change so I'm postponing writing any tutorials.

To stay on the topic, when working on symbolic/automatic differentiation I have realized few things:

• Partial derivative notation is often abused and used ambiguously for example Euler Lagrange equation is usually written in nonsensical way. I had to come up with a notation that can be fully formalized. Now it is much easier for me to understand the normal notation and spot if there is a mistake/ambiguity.
• Differential operator zoo: differential, partial derivative, derivative in a direction, total derivative, gradient, ... what is the exact relation between those? My realization is that all can be defined with differential and transposition. In particular, to define gradient you need to do transposition thus it make sense only if you have inner product.
• The main difference between symbolic and automatic differentiation is in how you handle let bindings.
• To differentiate a solution of an ODE w.r.t. the initial condition you need to solve its adjoint ODE. Discretizing this adjoint ODE gives you something very similar as discretizing the original ODE and applying back propagation.
• Adjoint connects together some basic functions on arrays. Example: adjoint of element acces of an array is Kronecker delta or adjoint of dropping an element of an array is pushing a zero element to an array.

I'm not claiming these are any new insights and often they stem from my ignorance/laziness studying literature properly. But I have found out that if I want to understand something properly it is often useful and faster to write it down in Lean, get the types right and distill the core of the problem in the process.

[Ben]

Nilesh said:

Oh, this is very interesting. Has someone attempted to formalize high-school or undergraduate physics? Laws of motion, gravitation, electromagnetism etc?

I've started cataloging various derivations for mathematical Physics -- see https://derivationmap.net/
That project doesn't currently feature formal verification (e.g., Lean) but does have some derivation steps validated by a Computer Algebra System (specifically SymPy).
In the past weeks I've started talking with @Tyler Josephson ⚛️ and his group about how to include Lean.

[Ben]

I wasn't previously aware of https://github.com/lecopivo/SciLean so I'll read more about that project as well.

[Tomas Skrivan]

Ben said:

I wasn't previously aware of https://github.com/lecopivo/SciLean so I'll read more about that project as well.

Please feel free to ask me any questions about SciLean if you have any.