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.
Coq is a formal proof management system. It is often referred to as a proof assistant.
316 questions
Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.
162 questions
Lean 4 is the latest major version of the Lean theorem prover by Microsoft Research. Use this tag for questions specific to Lean 4; if it's about Lean in general, use the tag (lean).
159 questions
for questions about type theories, which are formal systems to specify properties of objects.
93 questions
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
90 questions
For questions regarding Agda: the programming language / proof assistant.
69 questions
for questions about dependent types, which are families of types which vary over elements of another type.
55 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…
44 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…
42 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).
39 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)
39 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 …
37 questions
Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. If using the final "official" release from 2019 (3.4.2) which is incompatible with [mathlib], make thi…
34 questions
A proof assistant, or interactive theorem prover, is a software tool to assist with the development of formal proofs by human-machine collaboration.
33 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.
32 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 …
25 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…
25 questions
Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].
25 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 …
25 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…
24 questions
Questions asking how to properly and efficiently use Proof Assistants.
24 questions
for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.
22 questions
Tag for questions about induction such as mathematical induction, structural induction or well-founded induction (Noetherian).
22 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 …
21 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.
19 questions
For use with the proof assistant Isabelle with classical higher-order logic.
18 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…
17 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.
17 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…
16 questions
Use this for questions seeking an asset that give nebulous criteria rather than concrete specifics. If seeking literature such as books or papers use [tag:reference-request]. If seeking software use […
15 questions
For question about natural numbers $\Bbb N$, their properties and applications
15 questions
14 questions
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…
14 questions
For questions about words, phrases and definitions that are specific to proof assistants.
14 questions