Tags
A tag is a keyword or label that categorizes your question with other, similar questions. Using the right tags makes it easier for others to find and answer your question.
Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. The current version of Lean is Lean 4, so [lean4] is a synonym for [lean]. For question …
461 questions
The Rocq Prover used to be known as Coq. You should use the `rocq-prover` tag instead.
421 questions
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
144 questions
for questions about type theories, which are formal systems to specify properties of objects.
115 questions
The Rocq Prover is a proof assistant, that was previously known as Coq. This tag should be preferred to `coq`.
108 questions
For questions regarding Agda: the programming language / proof assistant.
84 questions
for questions about dependent types, which are families of types which vary over elements of another type.
74 questions
Mathlib is Lean's Math Library. The library is hosted on the GitHub
leanprover-community account. Do not use this tag for Lean the software. Do not use this tag for other math libraries of other pro…
65 questions
A tactic is a command or instruction for constructing a formal proof by applying a common proof technique. For questions about high-level techniques for constructing proofs, use the tag (strategy).
59 questions
with the proof assistant Isabelle, if your question is specific to a certain object logic please use the corresponding tag (eg. questions specific to Isabelle/HOL should also be tagged wi…
59 questions
A proof assistant, or interactive theorem prover, is a software tool to assist with the development of formal proofs by human-machine collaboration.
51 questions
In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)
50 questions
Questions pertaining to equality in type theory (all kinds of equality are included: judgemental, propositional, observational, setoid equality, etc.) and equality reasoning in proof assistants.
44 questions
if you are implementing a proof engine, proof assistant or something similar in code. Do not use this tag if you are just at the design stage or asking about design decisions of existing …
41 questions
Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. Only use this tag if your question is specifically about Lean 3. If using the final "official" release…
34 questions
Tag for questions about induction such as mathematical induction, structural induction or well-founded induction (Noetherian).
34 questions
used for questions that ask for software with a certain property or goal, such as automated theorem provers for equational logic. If the question is not specifically for software consider …
30 questions
Categories are structures containing objects and arrows between them. Many mathematical structures can be viewed as objects of a category, with structure preserving morphisms as arrows. Reformulating …
30 questions
Cubical type theory is a version of homotopy type theory in which univalence is not just an axiom but a theorem, hence, since this is constructive, has “computational content”. Cubical type theory mod…
29 questions
Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].
29 questions
In mathematics, and particularly in set theory, category theory, type theory, and the foundations of mathematics, a universe is a collection that contains all the entities one wishes to consider in a …
29 questions
For questions regarding ATP's (Automatic Theorem Provers), which attempt to prove a theorem without any assistance. If you are using a Proof Assistant or an interactive theorem prover and are providin…
28 questions
for questions about mathematical or logical foundations of proof assistants. Questions should be related in some way to proof assistants. Possible topics might include mathematical modell…
27 questions
Homotopy type theory is a flavor of type theory – specifically of intensional (Martin-Löf-) dependent type theory – which takes seriously the natural interpretation of identity types as formalizing pa…
26 questions
for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.
25 questions
For use with the proof assistant Isabelle with classical higher-order logic.
22 questions
The Cubical mode extends Agda with a variety of features from the CHM version of Cubical Type Theory. In particular, computational univalence and higher inductive types which hence gives computational…
22 questions
For question about natural numbers $\Bbb N$, their properties and applications
20 questions
20 questions
Calculus of (co)Inductive Constructions is a pure type system (Coquand, Huet) equipped with addition types:
arbitrary (co)inductive types implementing general (co)inductive schemes; universes as a cu…
20 questions
when a question is related to specifics on how a proof assistant works. Do not use this tag for questions related to using a proof assistant.
20 questions
Set theory is the branch of mathematics that studies unordered collections of objects. Questions with this tag will involve proofs about sets or operations on them.
20 questions
when asking a question that is not about a specific Lambda-calculus such as pure, typed, etc.
19 questions
19 questions