13
$\begingroup$

Can we collect (or maybe even write) tutorials and guides on doing analysis in various Proof Assistants? Community wiki style?

I was reading Lawrence Paulson's blog (highly recommend!) the other week and https://lawrencecpaulson.github.io/2021/11/17/Cauchy-Schwarz-example.html in particular. It employs pretty specific rules, tactics and theorems relevant to calculus.

I have an impression analysis-formalizing libraries for other proof assistants develop some specific tactics and notations too. For instance I looked over https://github.com/math-comp/analysis/ and https://github.com/lecopivo/SciLean

So the question is: where can I learn about that specifics?

For Program Analysis we have very comprehensive guides like Software Foundations, PLFA, Concrete Semantics and Functional Algorithms, Verified (plus their "fan translations" from one Proof Assistant to another). Do we have (or can we have) anything comparable for Mathematical Analysis?

A related but narrower question was mostly misunderstood and poorly answered as far as I can tell (but decided to mention for completeness).

Improve this question
$\endgroup$
15
  • 2
    $\begingroup$ There is a survey article about formalizing real analysis, which you might be interested in... $\endgroup$
    – Alex Nelson
    Commented Apr 10, 2022 at 18:22
  • 2
    $\begingroup$ Like, one of the half-dozen resources which may be interesting is John Harrison's PhD Thesis, which was focused on the different ways to formalize the real numbers in a proof assistant. It was around 150 pages, iirc, and worked within HOL Light. $\endgroup$
    – Alex Nelson
    Commented Apr 12, 2022 at 14:30
  • 1
    $\begingroup$ I did a quick search search of Lean community YouTube channel and found few videos about analysis. Calculus and integration: youtu.be/p8Etfv1_VqQ Topology and filters: youtu.be/hhOPRaR3tx0 Measure theory: youtu.be/yH3-zE0bYCU $\endgroup$
    – tom
    Commented Aug 23, 2022 at 19:29
  • 1
    $\begingroup$ I know very little about Hoare Logic, but from the quick look it looks similar to some kind of categorical reasoning. To do automatic/symbolic I mostly follow this paper arxiv.org/abs/1804.00746 which defines specialized categories for differentiation and rewrite rules for expressions in them. From my limited understanding, it looks like one could frame this in term of Hoare logic too. This would be quite specialized and only useful for computing derivatives. However, the paper is in Haskell, not theorem prover so not exactly what you are looking for. $\endgroup$
    – tom
    Commented Aug 25, 2022 at 20:53
  • 1
    $\begingroup$ Your question prompted me to write something down. It is more 'how to use symbolic differentiation in SciLean' but it can give you an idea how to do calculus computations in a theorem prover lecopivo.github.io/SciLean/doc/differentiation_in_scilean.html $\endgroup$
    – tom
    Commented Aug 30, 2022 at 21:12

1 Answer 1

Reset to default
4
$\begingroup$

I'm the author of the mentioned library SciLean and this question prompted me to write down a bit about how I do symbolic differentiation in Lean: Differentiation in SciLean (note: it is still work in progress)

It is more of a guide how to use SciLean to do symbolic differentiation rather then a guide how to build something like SciLean. Hopefully you can get the main idea from it and maybe get inspired.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.