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.
113 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.
76 questions
for questions about type theories, which are formal systems to specify properties of objects.
54 questions
For questions regarding Agda: the programming language / proof assistant.
45 questions
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
35 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 …
30 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).
26 questions
for questions about dependent types, which are families of types which vary over elements of another type.
24 questions
for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.
21 questions
Questions requesting papers or books in the literature on specific, narrow issues. Also consider the tag [recommendations].
21 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…
20 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)
20 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…
19 questions
Questions asking how to properly and efficiently use Proof Assistants.
19 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…
18 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 …
18 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.
17 questions
Mathlib is Lean 3'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 p…
16 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).
16 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…
15 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 …
15 questions
For questions about words, phrases and definitions that are specific to proof assistants.
13 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 …
13 questions
for questions about the logical concept of predicativism, which is the rejection of self-referential definitions, or impredicativity. This may be used to refer to the implementation of po…
12 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.
12 questions
The history of proof assistants and machine-assisted proofs.
12 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 […
12 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.
11 questions
A proof assistant, or interactive theorem prover, is a software tool to assist with the development of formal proofs by human-machine collaboration.
11 questions
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…
10 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…
10 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…
10 questions
when the question is about using a Proof Assistant for a purpose, how would you apply the Proof Assistant to solve a particular problem. Do not use this tag if it relates to a software ap…
10 questions
Use with coinductive types.
10 questions
For questions about constructive or intuitionistic logic. Constructive proofs can be extracted as programs.
9 questions
Universe polymorphism is the ability for definitions to be implicitly duplicated at different universe levels, with the types they contain. (from nLab).
9 questions
1
2 3 4 5
7