Generating random theorems

Stream: maths

[ElCondor]

I'm looking for a tool that would be able to generate random theorems in a given formal system (let's say a recursively axiomatizable first order theory like group/ring/field theory or Peano arithmetic), for instance by exploring a graph.

Do you know some open-source software that would do that?
Even better, if that could produce random theorems in Lean! (I suspect this is not very far from what some tactics like simp are actually doing)

[Adam Topaz]

Generating random theorems isn’t too hard. But generating random theorems that are not completely uninteresting is much harder.

[ElCondor]

Adam Topaz said:

Generating random theorems isn’t too hard. But generating random theorems that are not completely uninteresting is much harder.

I guess, still I'm curious to see what it would look like in practice.

[Terence Tao]

This isn't exactly the same, but a few months ago I posed a challenge of using automated tools to try to explore the graph of implications between equational laws involving a single binary operation: https://mathstodon.xyz/deck/@tao/110736805384878353 . (A portion of this graph can be found at https://mathoverflow.net/a/451008/766 .)

[Adam Topaz]

Maybe I should mention that I’m currently working on something like this. I don’t have anything to share publicly yet though

[Siddhartha Gadgil]

I don't know what your goals are but if you give GPT-4 a bunch of Lean theorems and ask it to generate more it comes up with a bunch (this idea is Adam Kalai's).