Questions tagged [provers]

Use this for a more general category that includes proof assistants, automated theorem provers and interactive theorem provers.

Filter by
Sorted by
Tagged with
9 votes
1 answer

Current status of cubical inductive families

I have the impression that cubical type theory hasn't dealt with inductive families yet. But the only source on this matter I can get is this Agda issue. What I've gathered is Agda supports defining (...
Trebor's user avatar
  • 3,490
20 votes
1 answer

Examples of formalisation of abelian categories

The question I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
Kevin Buzzard's user avatar
12 votes
1 answer

Learning materials for doing analysis (calculus) in a mechanized way

Can we collect (or maybe even write) tutorials and guides on doing analysis in various Proof Assistants? Community wiki style? I was reading Lawrence Paulson's blog (highly recommend!) the other week ...
Alex Chichigin's user avatar
6 votes
0 answers

Is any theorem prover able to prove quadratization relations without knowing the proof strategy that humans used?

Motivation In discrete optimization, our goal is often to optimize a function of binary variables, such as: $$\tag{1} {\scriptsize 5 - 3b_1 - b_2 - b_3 + 2b_1b_3 - 3b_2b_3 + 2b_1b_2b_3 - 3b_4 + ...
Nike Dattani's user avatar
  • 1,105
3 votes
4 answers

What provers are using quote, quotations or quasiquotations?

This is a related question to Is there a consolidated or partial list noting the use of quasiquotation with provers? for which it seems there is no answer. However as there might be an answer some ...
Guy Coder's user avatar
  • 2,796
6 votes
0 answers

Is there a consolidated or partial list noting the use of quasiquotation with provers?

In checking to see if any provers (proof assistants, theorem provers, interactive theorem prover) make use of quasiquotation I was quickly surprised at what started showing up with a Google search. ...
Guy Coder's user avatar
  • 2,796