# Tag Info

## Hot answers tagged beginner

### Proof assistants for beginners - a comparison

Lean I am a professional mathematician with minimal experience in coding or computer science (and who has no idea what "leftpad" is ;-) ), and I personally found it very hard to break into ...
• 2,510

### Proof assistants for beginners - a comparison

Coq The easiest proof assistant to start with is The assistant with the best learning resources The assistant with a great community The assistant with the nicest libraries in that order of priority....

### Proof assistants for beginners - a comparison

I believe it will depend a lot on your experience and sensibility, but that a good way of getting started is to have a look at lets-prove-leftpad : This is a repository of provably-correct versions ...
• 321
Accepted

### Tools for checking the consistency of a type theory

One can think of type theory as an algebraic theory on steroids (there is technical merit to this claim). Every algebraic theory has a model, namely the trivial one whose carrier is the singleton. A ...
• 9,842
Accepted

### What is the difference between refl and rfl in Lean 3?

So you are correct that refl is a tactic, and rfl is a term, so for example: ...
• 1,445

### Proof assistants for beginners - a comparison

I'll answer the question "What is the easiest proof assistant to start with for a programmer" and take the sub-questions one-by-one. Which one is the easiest to pick as a language? Agda, ...
• 261

### Proof assistants for beginners - a comparison

(This answer was originally for another question, but others thought it was better as an answer for this question, or for this question.) I think for these sorts of questions it depends a lot on your ...
• 9,360

### Proof assistants for beginners - a comparison

The Incredible Proof Machine There is no need to learn syntax to enter, you just drag and drop boxes and connect them, and still learn a lot about rigorous proofs, intro and elim rules, local ...
• 1,914
Accepted

### Explanation of Coq math-comp repositories

As Meven wrote, the Mathematical Components repositories originate from the work of Georges Gonthier and his team proving first the Four Color Theorem, then the Odd Order Theorem. In Coq people do not ...
• 637
Accepted

### What is the current state of proof assistants?

These are broad questions and I doubt you will get a complete answer in a single stack exchange answer. But since you seem ernest and interested, let me at least try to help clarify some of your ...
• 9,360
Accepted

### Representing $\Bbb RP^2$ in Lean: building a type representing a particular set

Let me answer your immediate question first with the following code snippet (which relies on mathlib): ...
• 166

### Proof assistants for beginners - a comparison

The part of your answer I like best is a "Python of proof assistants". :) When I see "Python" I read "a programming language which is deceptively simple on the surface level ...

### Strong induction on ℕ with function α → ℕ

Here's how to prove Andrej Bauer's corrected statement using the induction tactic: ...
• 971

### Explanation of Coq math-comp repositories

Roughly, Mathematical Components are a set of libraries that are designed to work together, and follow a lot of common ideas and guidelines, in particular the use of the SSReflect proof language, ...
• 5,530

### Formalizations of unsolved problems

The closest to what you are asking for might be the Formal abstracts project whose aim is to formalize the statements (but no proofs) of results from papers. Formalizing statements without proofs is ...
• 9,842
Accepted

### How to replace a function by its body

The tactic you are looking for is probably unfold. If you write unfold bexp it will replace it with its body. In certain cases, ...

### Proof assistants for beginners - a comparison

The main issue with this question is that it asks to compare proof assistants on several points but people who answer cannot know enough about all proof assistants to make this comparison point by ...

### What is the difference between refl and rfl in Lean 3?

Separately from the rfl (term) vs refl (tactic) distinction, there is also the distinction between ...
• 971
Accepted

...
• 9,842
Accepted

### How to define curry in Lean

If Lean checks your code you know it is correct. (Well, that and the fact there is only one curry function up to functional equivalence.) Now as for how to use ...
• 9,360

### How do I express a negative premise in Coq?

This is not a Coq issue. Rather, Coq rightfully complains that a relation such as the one you envision might not be well-defined. Indeed, suppose you had another (perfectly valid) premise ...
• 5,530

### Why is $\Bbb Z = \Bbb N$ independent of Lean?

It suffices to give two models of Lean's type theory, one in which $\mathbb{Z} = \mathbb{N}$ and another in which $\mathbb{Z} \ne \mathbb{N}$. We shall use the interpretation of Lean type theory in ...
• 9,842
Accepted

### Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

Follow the structure of the function you are proving things about. Looking at the definition of Ascii.eqb (shown below), it is defined using ...
• 2,032
Accepted

### How do you import part of the standard library in Coq?

The recommended import to get the many lemmas associated with nat is Require Import Arith. This includes ...
• 2,032
Accepted

### What mathematical topics should I learn first before I start using proof assistants?

I came to proof assistants from TCS about a year ago, so perhaps I am well placed to answer your question. This may be somewhat opinion-based, but I don't feel it is necessary to learn category theory ...

### Comparison between proof assistants for coinductive structures and proofs

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet. Coq: ...
Accepted

### Coq defining a hierarchy of collections of integers with infinitely many "levels"

A simple way is to define the type in terms of the Peano natural numbers nat. ...
• 684

### Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

I mean, it's still exhaustive case analysis, but intros [[] [] [] [] [] [] [] []]; reflexivity. at least is shorter. If you use ...
• 609

### What mathematical topics should I learn first before I start using proof assistants?

I would say the most confusing (and often frustrating) notion for many first users is that types are not sets, so unless you plan on using a proof assistant specifically based on set theory (almost ...
• 2,320
The extra fields are a convenience. It is useful to have both $<$ and $\leq$ at disposal when working with preorders, so how can we have that? We could decide which one is “primary”, include it in ...