What are...computer conjectures?

Goal.
I would like to tell you a bit about my favorite theorems, ideas or concepts in mathematics and why I like them so much.
This time.
What are...computer conjectures? Or: A computer can write poems, so...
Disclaimer.
Nobody is perfect, and I might have said something silly. If there is any doubt, then please check the references.
Slides.
www.dtubbenhauer.com/youtube.html
TeX files for the presentation.
github.com/dtubbenhauer/My-Te...
Thumbnail.
media.wired.com/photos/595490...
Main discussion.
www.taylorfrancis.com/books/m...
www.nature.com/articles/s4158...
www.sciencedirect.com/science...
www.sciencedirect.com/science...
en.wikipedia.org/wiki/Categor...
formalabstracts.github.io/
cmartinez.web.wesleyan.edu/do...
www.ams.org/notices/202011/rn...
www.ams.org/notices/200811/tx...
www.quantamagazine.org/how-cl...
math.stackexchange.com/questi...
arxiv.org/abs/math/9404236
link.springer.com/article/10....
www.nature.com/articles/d4158...
www.jstor.org/stable/2025805
sites.math.washington.edu/~bi...
link.springer.com/book/10.100...
calculemus.org/MathUniversali...
Background material.
en.wikipedia.org/wiki/Proof_a...
en.wikipedia.org/wiki/Automat...
en.wikipedia.org/wiki/Compute...
en.wikipedia.org/wiki/Automat...
en.wikipedia.org/wiki/Artific...
en.wikipedia.org/wiki/Mathema...
en.wikipedia.org/wiki/Compute...
en.wikipedia.org/wiki/Formal_...
en.wikipedia.org/wiki/Compute...
Computer talk.
en.wikipedia.org/wiki/Categor...
reference.wolfram.com/languag...
Pictures used.
en.wikipedia.org/wiki/Birch_a...
Pictures of Magma output magma.maths.usyd.edu.au/magma/
transportgeography.org/wp-con...
Pictures from www.sciencedirect.com/science...
Picture from www.nature.com/articles/s4158...
KZbin and co.
• Thomas Hales: Formal A...
• Georges Gonthier: Comp...
#logic
#computerscience
#mathematics

[@eternaldoorman5228]

That was really interesting. I came here from your most recent algebraic graph theory video because I was thinking about the work of Cvetkovic who has written hundreds of papers on theorems which were 'inspired' by a computer model called GRAPH. Whether it is the program that produces the actual conjectures or whether it is the mathematician who sees the patterns in the data which trigger mathematician to conceive the conjectures I don't know. But I think what is a good conjecture depends heavily on your philosophy of mathematics. If you think of a mathematician as an individual wandering a vast space of possible mathematical theorems and getting to know some corners of it very well and describing them to the outside world in learned journals the world of mathematics is just forever going to become more and more complicated and intractable, to my mind. So I am more interested in mathematics which unifies fields and shows that these two things, graph theory and linear algebra, for example, are to some extent _the same thing_ and elucidating exactly what is meant by that sense of 'sameness'. These are the sorts of things that I find really interesting and so when I started to get a glimpse of what Category theory is all about I thought "This is really interesting! These people have got _mathematical methods_ of elucidating exactly what it means to say that two abstract undefined things are the same! But whenever I (try to) read a book about Category theory I see that instead of explaining how mathematics is unified, they are just exploring yet another vast, but even more recondite space of infinite-dimensional objects or something and so what should have been a unifying principle has become another divergence. I can't help but wonder if this isn't an effect of research funding at Universities. So that's how I got interested the idea of univalence and translations of languages. That's the level at which I think computers are most useful: formalising in a concrete, testable manner, exactly what we mean by some particular interpretation of a language, and elaborating the sentences in those languages. So I can get to the point I wanted to make in this comment, which is that it is often the definitions that are the really creative aspect of mathematics. The definitions are what sets the stage for the theorems you can prove, because they are all expressed in terms of those definitions, and so any conjecture is also expressed in terms of the definitions. So to take that list of computer-generated conjectures at the end of this video, each one is expressed in terms of some defined property of a graph such as dimension, rank, etc. And the kind of unifying process I imagine is more like one where we change those fundamental definitions and for any given model essentially the same elaboration then produces a completely different list of conjectures because the definitions have changed underneath the enumeration process.

[@eternaldoorman5228]

A slightly tangential thing: I often wondered how it was that someone like Jacques Herbrand could come up with the theorem that bears his name, without actually having a proof to hand, because it turned out that the proof he himself presented was actually flawed, so it was really Herbrand's _conjecture_ until some time after his tragic death. I wondered, because I am actually a very uncreative person, mathematically. I cannot see something of mathematical interest unless I have _some idea_ of how it might be proved. So what I would like is a way of making proof (even formal proof) almost automatic in the process of constructing a mathematical expression. Herbrand's theorem is an intersting example of a kind of iterated quotient operation applied to a space.

[@VisualMath]

Thank you for these two comments! - Yes, math research, and research in general, is often or mostly guided by what is funded/popular and not so much by more intrinsic reasons. Whether this is regrettable or not is not clear; one advantage of the current model is the amount of produced research papers. Even if you argue that 99% are “useless”, including 100% of my own papers, then there is still plenty of good stuff left. - The state of the arts of automated conjecturing is a bit unsatisfying. I think this goes beyond the previous point and is related to what you mention: “What is a good conjecture?” appears to be very difficult to answer. - In contrast, automated proofs are in a fairly good state, despite the fact that this area is not super likely to get funded. - I sadly have essentially no intuition for logic, so I am also unsure how Herbrand and others came up with their fantastic result. Most of the time some form of examples are involved, with the meaning of “example” being context depending.

[@stoutes]

great topic and video!

[@VisualMath]

Glad you liked it! Or rather them - topic and video ;-) More important, I am glad that you like the topic - one of my favorites which needs to be developed further!

[@paulpetricevic6949]

awesome video!

[@VisualMath]

Thank you so much. But it is also an awesome topic ;-)

[@bhnjhbjhbkgkkvhnhmbm]

I was thinking about this lately. So for the state of the art AIs, we theach them things and then ask them questions. We should train a language model that thinks in Gödelian sentences, and can genarate more true sentences. This can be applied as building blocks for proof writing for existing problems, which are millenial for a reason.

[@VisualMath]

Yes, the state of the arts could/should be improved in many ways.