Skip to main content

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
0 answers
47 views

Bounding Volume Proof Assistant Library

I am interested in learning Lean/Coq/Isabelle etc. and wanted to try to formalize Joseph O'Rourke's Minimum Bounding Box Algorithm. I do not have much experience with proof assistant tools. Is there a ...
WakkaTrout's user avatar
0 votes
1 answer
258 views

How to use the most bare essentials of Lean 4?

As a learning exercise I want to use Lean 4 to prove theorems about natural numbers, but WITHOUT Mathlib (or as little as possible). I want to start with 2 Peano theorems s(x) != 0, and s(x)=s(y) ->...
Lewis Baxter's user avatar
3 votes
1 answer
119 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-...
Jorge Agra's user avatar
3 votes
1 answer
754 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 ...
Jack Maloney's user avatar
7 votes
3 answers
552 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 ...
anime cat girl's user avatar
5 votes
1 answer
164 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 ...
nilo de roock's user avatar
13 votes
1 answer
246 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 ...
Alex Chichigin's user avatar
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 ...
hardmath's user avatar
  • 539
12 votes
3 answers
624 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, ...
Colas's user avatar
  • 221
23 votes
1 answer
355 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 ...
GraffL's user avatar
  • 471
20 votes
9 answers
535 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 ...
postmortes's user avatar
18 votes
2 answers
256 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 ...
Bubbler's user avatar
  • 674
14 votes
3 answers
823 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 ...
Glorfindel's user avatar
54 votes
10 answers
8k 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 - ...
Piotr Migdal's user avatar