The tag has no wiki summary.

learn more… | top users | synonyms

2
votes
0answers
20 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. ...
2
votes
1answer
43 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 ...
7
votes
2answers
165 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 ...
0
votes
0answers
44 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 ...
2
votes
2answers
133 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 $$ ...
36
votes
12answers
3k 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.
3
votes
0answers
38 views

Tool for construction of graph with specified properties

Is there a tool (class of algorithms for graph generation) that can construct graph with specified properties. E.g. construct graph who is homeomorphic with both to K5 and K3,3. Construct planar graph ...
6
votes
1answer
152 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 ...
0
votes
1answer
52 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 ...
0
votes
0answers
66 views

Can a Computer Algebra System 'experiment' with expressions?

I have recently been reading about software for symbolic manipulation, and I can see its use as a tool for performing large calculations that would be unfeasible otherwise. Given that these systems ...
6
votes
1answer
98 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 ...
0
votes
0answers
33 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 ...
6
votes
1answer
86 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 ...
2
votes
0answers
93 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 ...
5
votes
2answers
135 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 ...
5
votes
0answers
65 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 ...
1
vote
0answers
250 views

Online math tool for equation visualisation

I am looking for a math editor that is able to present equations and relations between them. I am not searching for a traditional Latex / MathML editor (I know about various online services that allow ...
3
votes
3answers
209 views

Computer Assisted proofs apart from the 4 color theorem

I recently read about the 4 color theorem and that it was proved using help from computers. Does anybody know of some other 'good' computer-assisted proofs apart from the 4 color theorem?