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.
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.
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).
for questions about type theories, which are formal systems to specify properties of objects.
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
For questions regarding Agda: the programming language / proof assistant.
for questions about dependent types, which are families of types which vary over elements of another type.
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…
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…
In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)
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).
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 …
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…
A proof assistant, or interactive theorem prover, is a software tool to assist with the development of formal proofs by human-machine collaboration.
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.
Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].
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…
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 …
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 …
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…
Questions asking how to properly and efficiently use Proof Assistants.
Use with coinductive types.
for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.
Tag for questions about induction such as mathematical induction, structural induction or well-founded induction (Noetherian).
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 …
For use with the proof assistant Isabelle with classical higher-order logic.
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.
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.
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…
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…
For question about natural numbers $\Bbb N$, their properties and applications
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 […
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…
The history of proof assistants and machine-assisted proofs.
For questions that ask about possible improvements of a working piece of a proof. Make sure to also include the tag for the language used, and follow that tag's guidance regarding additional version-s…
For questions about words, phrases and definitions that are specific to proof assistants.