3

The notion of automating mathematics is a vague one, and that's accounting for the discrepancy here. One interpretation would be: to automate mathematics would be to produce a machine $M$ which could tell whether or not a given sentence is true (or, more weakly, provable from some agreed-upon set of axioms like $\mathsf{ZFC}$). Even the weaker version is ...


3

You do not have to prove things by induction. For example, you can prove $\forall n : \mathbb{N} \,.\, n = n$ without induction by applying reflexivity. In your proof, we use induction on $a$, but then we do not need to use induction on $b$ and $c$ because we can finish the proof simply using other methods. We could have used induction on $b$ and $c$, and ...


3

In your case, the simplest solution may be to use SAT. Your first clause includes $x \le 0.25$ and $x > 0.91$. This means that there are five regions of interest for the variable $x$, which we identify with boolean variables: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in ...


2

Yes, you could solve this with a SMT solver that supports linear real arithmetic. However SMT supports more general inequalities where you can have linear sums of variables (e.g., $2a+3x \le 5.7$) instead of simple comparisons between a single variable and a constant (e.g., $a \le 1.6$), so it might be more powerful than you need, so if you don't have any ...


2

You are conflating two possible meanings of the phrase "mathematics can be automated": "any theorem can be proved true or false by an algorithm" "the practical activity of proving theorems, as presently performed by humans, can instead be performed by computers in an economically-viable fashion" Due to the halting problem, it is impossible for any ...


1

Now let $\alpha$ be a pure word with $n_j$ symbols of degree $d_j$. It is easy to prove inductively that: $n_0 + n_1 + n_2 + ... = 1 + 0.n_0 + 1.n_1 + 2.n_2 + ...,$ i.e. $n_0 = 1 + n_2 + 2n_3 + ...$ I think there is a small mistake here, since $n_j$ should be considered as the number of symbols of degree $j$ and not of degree $d_j$ in $\alpha$. $n_0 + n_1 +...


1

While "disappointing in practice" is certainly not definable formally, unlike "complete" (which does indeed mean "can eventually prove every true formula"), it's pretty easy to find examples where naive resolution is not even remotely adequate, i.e. examples which should be easy to prove but which resolution is extremely slow on....


1

Look at Agda [1][2] I think that it's exactly what you are looking for. I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html A very good introduction is plfa [3], also [2]/tutorial-list.html [1] https://en.wikipedia.org/wiki/Agda_(programming_language) [2] https://agda.readthedocs.io/en/v2.6.0.1/getting-...


Only top voted, non community-wiki answers of a minimum length are eligible