# Tagged Questions

For questions regarding the different ways to generate and verify theorems via specialized computer languages, algorithms, and other computer-aided tools.

80 views

### define the “optimal” automatic theorem prover

my question is : is it possible to define in some way what should do an "optimal automatic mathematician" ? There are two points of view of an automatic theorem prover / automatic mathematician : ...
51 views

### From a set of rules, derive the implications?

I've only just become interested in this domain, so sorry if I'm not using the correct terminologies. What I want is the following: Say I have a set of rules (or constraints), I want to derive some ...
17 views

### Equivalence classes of $\{ij\ |\ i, j ∈ \{a, b\}^* , i \neq j\}$

I want to find the equivalence classes (Nerode-relation) of this language: $L = \{ij\ |\ i,j \in \{a,b\}^*,\ i \neq j\}$ It says that this language is regular and that it has 2 equivalence classes, ...
75 views

### An Auto-Generated Cartography of Mathematical Theories: Has it been done already?

While looking for a way to visualize the logical structure of mathematical theories a graph-like depiction came to my mind, where propositions are represented by vertices. An edge goes from ...
67 views

### Could mathematical reasoning be non-axiomatic?

"Mathematics is not a deductive science—that's a cliché. When you try to prove a theorem, you don't just list the hypotheses, and then start to reason. What you do is trial and error, experimentation, ...
94 views

### Status of declarative proof languages in proof assistants

I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order ...
63 views

### Is it useful to learn to use automatic theorem provers?

I mean, do ATP's spot some obvious errors in computations or proofs? And if I'm not sure about the correctness of some modern proof found in some article, say for example Mochizuki's proof of the ABC ...
95 views

232 views

### Coq transparency issues with type class fields

I am having some issues with, I suspect, transparency of fields in type classes. Consider a type class such as ...