Return to Answer

I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-simensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.

The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.

Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.

(Update:) One theorem proved by Gunter Meisinger, Peter Kleinschmidt and me was that every 9-polytope has a 3-face eith at most 77 facets. The proof was transformed into art by artist Bernard Venet.

I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-dimensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.

The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.

Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.

(Update:) One theorem proved by Gunter Meisinger, Peter Kleinschmidt and me was that every 9-polytope has a 3-face with at most 77 facets. The proof was transformed into art by artist Bernard Venet.

I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-simensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.

The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.

Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.

(Update:) One theorem proved by Gunter Meisinger, Peter Kleinschmidt and me was that every 9-polytope has a 3-face eith at most 77 facets. The proof was transformed into art by artist Bernard Venet.

I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-simensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.

The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.

Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.

(Update:) One theorem proved by Gunter Meisinger, Peter Kleinschmidt and me was that every 9-polytope has a 3-face eith at most 77 facets. The proof was transformed into art by artist Bernard Venet.

I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-simensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.

The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.

Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.

I have one personal experience with experimental mathematics. It started with a computer assisted simple proof of a result that every five dimensional polytope contains a 2-simensional face which is a triangle or a quadrangle. It turns out that the negation of this theorem implies a certain number of inequalities for the so called flag numbers which together with known inequalities lead to a contradiction. At the end the proof can be checked easily by hand.

The next step was with Gunter Meisinger and Peter Kleinschmidt (see this paper), and we made a computer program called FLAGTOOLS that was able to prove automatically theorem of a similar type. At a later stage we tried to let the program test systematically for such theorems. Among the theorems we proved is the following: that there is a finite list of 3-polytopes so that every 9-polytope has a face from that list. Some similar work for quasisimplicial polytopes which had additional features of automations were carried out by Shahar Lovett.

Overall, it was difficult to use the automatic systems to obtain unanticipated "meaningful" or "interesting" results, and this had become harder the higher the level of automation was.

(Update:) One theorem proved by Gunter Meisinger, Peter Kleinschmidt and me was that every 9-polytope has a 3-face eith at most 77 facets. The proof was transformed into art by artist Bernard Venet.