Tagged Questions

The tag has no usage guidance.

464 views

What is the current state of formalized mathematics?

Russell and Whitehead famously tried to actually create and use a formal system to explicitly develop formal mathematics in their work, "Principia Mathematica." Much more recently, with the aid of ...
277 views

How do I find an inverse of any element in any group?

I'm working on Agda, which is based on intuitionistic type theory. I defined groups in Agda with normal laws of groups, which (of course not only) says that there is an inverse element of every ...
48 views

Symbolically formulate the two guard problem so it can be solved by a computer

Take the classic two guard riddle (I don't know where the origin of this riddle is, so I'll take the version from http://www.calpoly.edu/~mcarlton/riddles.html): You stand at a fork in the road. ...
47 views

Is there any Software package to confirm correctness of your derivation steps?

Suppose I made a very complicated (not necessarily difficult) derivations in which it is very likely for anyone to make some silly mistakes, e.g., incorrect sign, overlooking a term, and so on. I ...
353 views

Examples of the benefits of Homotopy Type Theory for computer aided proofs?

From what I understand, Homotopy Type Theory is proposed as a new foundation of mathematics, and it supposed to be superior for use with computer aided proofs. I am currently trying to understand the ...
47 views

$x^4-x \in Z(R)$ implies commutativity [duplicate]

Let $R$ be a ring and $Z(R)$ the centre of $R$. There exist elementary proofs (that is, proofs not using the structure theory of rings) of the fact that if $x^n-x \in Z(R)$, then $R$ is commutative ...
137 views

Are there explicit forms of these integrals

Let $a>0$, and $z_0=r_0e^{i\theta_0}$, where $0<r_0<a$, $0<\theta<\gamma<\frac{\pi}{2}$, do we have a closed form of each of the following integrals  I_1(r_0,\theta_0)=\int_{0}^{a}...
4k views

What are some theorems that currently only have computer-assisted proofs?

What are some theorems that currently only have computer-assisted proofs? For example, there's the four colour theorem. I am very curious about this and would like to generate a list.
284 views

Numbers as sum of distinct squares

Yesterday Polish Olympiad of Information Science ended, one of the questions was purely mathematical, Squares (PL). In the task, we have defined square ...
69 views

Understand a Maple output

My goal is to solve for $L$ in $\frac{(2k)!}{2^kk!}{2nL - L^2 \choose 2k} = \sum_{s=0}^k{L \choose s}{n-L \choose s}s!\frac{(2k-2s)!}{2^{k-s}(k-s)!)}{L-s \choose 2k-2s}.$ I tried to use the solve ...
128 views

Where can I download the approx 1500 Appel-Haken reducible configurations in the Four-Color-Theorem proof?

Where can I download computer representations of the approximately 1500 Appel-Haken reducible configurations in the Four-Color-Theorem proof? The Wikipedia article (http://en.wikipedia.org/wiki/...
41 views

A conjecture on the product of digits of a number

Define $(m,n)$ to be a special pair if $n=m \cdot Pd(n)$. Where $Pd(n)$ is the product of digits $n$. Then I have the following conjecture - For every $m$ with no digit of $m$ being $0$ , there ...
96 views

Math via Computers

What computer language is best for doing mathematics? That is, which of C or Ruby or whatever would generally be the widest applicable efficient computer language to master for doing mathematics? In ...
128 views

Cut-off Subtraction in Coq

I am new to the world of computer assistant proof programs in general, and Coq in particular. As a result, I have sought to prove some elementary results about integers as a way to … At the moment, I ...
143 views

What is the meaning of proof of a proof?

After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof. We can express proofs as a computer program Proof is correct ...
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 ...