Skip to main content
24 votes
Accepted

Why should you "never resort to polymorphism when initiality would do"?

Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of ...
gallais's user avatar
  • 1,256
18 votes

What are the advantages to impredicativity?

All impredicativity means is that propositions form a complete lattice! This is a basic principle of mathematics. So if you want to be able to use the architecture of mathematics developed in the last ...
Neel Krishnaswami's user avatar
10 votes

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

There is no single right answer and all of this will be highly subjective. Before I get into the details based on the subjects you want to learn, I would just say, pick something, play around with it,...
Jason Rute's user avatar
  • 8,960
8 votes
Accepted

What are the advantages to impredicativity?

There are some tricks that only work when you have access to an impredicative universe. They tend to construct "the smallest object" of some kind, without an explicit construction, i.e. a ...
Pierre-Marie Pédrot's user avatar
7 votes

Counterexamples in Type Theory

Coq maintains a document of historical proofs of absurdity, including brief explanations of the flaw that allowed them to pass. Most of these are more "counter-examples in type theory ...
Jason Gross's user avatar
  • 1,537
7 votes

Inductive vs. recursive definitions

Defining recursive properties by fixpoint is possible, but it is usually easier to reason on inductively defined ones. Mostly because they come with their own induction principles. If you use fixpoint ...
Pierre Courtieu's user avatar
7 votes
Accepted

Pragmatic encodings of inductive inductive types

Your example signature is negative recursive in the second field of Sigma so it can't be encoded in total languages. For internal universes, the usual solution is ...
András Kovács's user avatar
6 votes

Figures on computer proof assistant usage

I don't have answers to most of your questions but another way to look at this question is which proof systems have formalized the most theorems. The largest scale effort that I know of to track ...
Jim Kingdon's user avatar
6 votes
Accepted

How can you represent a dependent type visually?

I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this: Please look at the slides for ...
Andrej Bauer's user avatar
  • 9,593
6 votes

Why is it hard to formalize informal proofs?

Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc? Yes: we don't know what we actually do when we mentally verify equations! This is a glib ...
Neel Krishnaswami's user avatar
6 votes
Accepted

Naming conventions (letter case, underscores, &c) for Coq

A similar question was recently discussed in the Coq Zulip chat (regular link, no-login-needed link), of which this answer is a summary. The vstyle project is working on building / collecting Coq ...
Ana Borges's user avatar
5 votes
Accepted

Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

Building that gigantic proof graph as an explicit graph would probably be a very bad idea, given its size and the complexity of "connecting inputs to outputs". Indeed, as you can have an ...
Meven Lennon-Bertrand's user avatar
4 votes

Counterexamples in Type Theory

Making this a community wiki. Here are a few that come to mind, some more obvious than others, with a theme, and not described in detail. May add more later. A simply typed $\lambda$-term whose ...
4 votes

Inductive vs. recursive definitions

Let me just mention a third possibility which is sometimes called "small inversion". This is some kind of middle ground between the two possibilities you present, which gives you some of the ...
Meven Lennon-Bertrand's user avatar
3 votes

Counterexamples in Type Theory

As mentioned in this answer on this site, so-called "positive coinductive types" break subject reduction.
3 votes
Accepted

Figures on computer proof assistant usage

I think one has to be a bit careful here. I wouldn't say the primary users of proof assistants would self identify as mathematicians. I think many use proof assistants for software and hardware ...
Jason Rute's user avatar
  • 8,960
3 votes

Pragmatic encodings of inductive inductive types

To complement András' answer, and especially if you want to stay in Coq, you can also define such an internal universe using indexed inductive types only. Basically, you replace the definitions of ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

(This answer assumes you already know some of the basics of Lean as in Theorem Proving in Lean 4.) In a typical first logic class or set theory class in college, first order logic is presented as ...
Jason Rute's user avatar
  • 8,960
3 votes

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

I really cannot improve on Jason Rute's answer, but one suggestion I would have: after playing around with whatever theorem prover you decided to use, dabble around with a few others. In particular, ...
Alex Nelson's user avatar
  • 1,574
2 votes

Inductive vs. recursive definitions

Inductive allows you to express non-deterministic, non-terminating computations, while Fixpoint computations can be ...
tarzh's user avatar
  • 291
1 vote

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

I can't (yet) recommend AutoMath, except for historical interest. But, I resurrected it here AutoMath (GitHub) on GitHub, with upgrade on its syntax. Its biggest weakness, by far, is its inability to ...
NinjaDarth's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible