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
3 votes
1 answer

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-...
Jorge Agra's user avatar
3 votes
1 answer

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 ...
Jack Maloney's user avatar
6 votes
3 answers

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 ...
anime cat girl's user avatar
5 votes
1 answer

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 ...
nilo de roock's user avatar
12 votes
1 answer

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 ...
Alex Chichigin's user avatar
17 votes
1 answer

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 ...
hardmath's user avatar
  • 539
9 votes
2 answers

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, ...
Colas's user avatar
  • 191
23 votes
1 answer

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 ...
GraffL's user avatar
  • 471
20 votes
9 answers

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 ...
postmortes's user avatar
18 votes
2 answers

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 ...
Bubbler's user avatar
  • 674
14 votes
3 answers

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 ...
Glorfindel's user avatar
44 votes
9 answers

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 - ...
Piotr Migdal's user avatar