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.
12
questions
3
votes
1
answer
111
views
Metamath - simple equation solution / proof
Sorry if an improper question, looking into metamath and metamath-lamp and though it should be trivial to prove A = 2 -> ( A + 2 ) = 4, or the inverse.
But cant seem to get it right in metamath-...
- 55
3
votes
1
answer
409
views
Using the contrapositive in lean 4
I'm trying to learn lean (version 4) by proving some basic facts about the natural numbers. Please feel free to critique my code if you see have general comments, but I also have a specific question ...
- 133
6
votes
3
answers
522
views
How are the parts of category theory which make explicit reference to Set different when formalized in a proof assistant that is based on type theory
In category theory a presheaf is defined as a functor whose target is $\mathrm{Set}$, and the concept is used to state the Yoneda lemma. The appearance of $\mathrm{Set}$ in the definition comes from ...
5
votes
1
answer
146
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 ...
- 151
12
votes
1
answer
231
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 ...
- 654
17
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 ...
- 539
9
votes
2
answers
382
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, ...
- 191
23
votes
1
answer
304
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 ...
- 471
20
votes
9
answers
491
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 ...
- 319
18
votes
2
answers
223
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 ...
- 674
14
votes
3
answers
646
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 ...
- 711
44
votes
9
answers
5k
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 - ...
- 581