Questions tagged [learning]

Learning covers topics such as how to install, how to choose a proof assistant, working through tutorials. For using a proof assistant consider the usage tag along with a specific proof assistant like Coq, Lean, MetaMath, etc.

Filter by
Sorted by
Tagged with
4 votes
1 answer
85 views

Looking for an entry point in the universe of proof assistants and proof IDE's

This is my first question in this part of StackExchange. What I would like to achieve is the following. Suppose I want to study ( or give a course on ) basic Real Analysis, I want to 1) document the ...
user avatar
9 votes
0 answers
114 views

Learning materials for doing analysis (calculus) in a mechanized way

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 ...
user avatar
16 votes
1 answer
1k views

So many data types, so little time

I find my mathematics and programming background$^*$ do not endow me with much understanding of type theory as it pertains to proof assistants. To remedy this shortcoming I don't expect a Royal Road ...
user avatar
  • 509
8 votes
2 answers
281 views

Which proof assistant would you advise me to learn (in 2022) considering my interests?

I am a math teacher in college. I’m very interested in type theory. So far, I got the general idea of it but I would like to go deeper. I am interested in philosophy of maths, in foundations of maths, ...
user avatar
  • 181
19 votes
1 answer
144 views

Tutorials for formalizing mathematical definitions/statements in Lean

tl;dr: Are there any good introductions/tutorials on how to formalize definitions and theorem statements in Lean? (in contrast to introductions on formalizing proofs) Some background: I am a phd ...
user avatar
  • 421
18 votes
9 answers
377 views

What are good books for learning about proof assistants for Functional Analysis?

I did search on the site already and while there are questions that reference, for example, PLFA for Agda, there doesn't seem to be a canonical list of references for people just learning about proof ...
user avatar
17 votes
2 answers
154 views

Has there been any attempt at a tutorial that doesn't start with natural numbers?

The most well-known tutorials/learning materials, including Book 1, Chapter 2 of Software Foundations for Coq and the Natural Number Game for Lean, use natural numbers to introduce induction. But ...
user avatar
  • 664
13 votes
3 answers
331 views

Which programming languages are most similar to proof assistants?

Related to What is the easiest proof assistant to start with? – I suppose familiarity with programming in general would be beneficial to learning how to work with proof assistants. But which kind of ...
user avatar
31 votes
8 answers
906 views

Proof assistants for beginners - a comparison

What is a good starting point to learn about proof assistants? The answer will invariably depend on the area of interest: mathematics (and its areas, e.g. algebra,combinatorics, analysis, logic), CS - ...
user avatar