Automated Math Prove Synthesizer without Deep Learning

Stream: Machine Learning for Theorem Proving

[Gridiron Player]

Although this is symbolic AI and not machine learning, I just wanted to bring to attention what Victor Taelin is doing with automated theorem proving. This stuff is truly incredible and the future.

Also, he is looking for talents to join him. If somebody here is passionate about building out an automated theorem prover without deep learning, please reach out to him. He seems to have issues to find talented people.

https://x.com/VictorTaelin/status/1881392823246729640

In short:

He built a massively parallel compiler based on interaction nets that enables true type enumeration and very fast program / proof synthesis based on logical constraints and / or input and output examples. Truly incredible stuff.

[Jason Rute]

Thanks. Note this is discussed also here: #general > SupGen

[Gridiron Player]

Nevermind!

[Jason Rute]

No, it is good to make sure relevant folks are aware. (If you know Victor, have him interact here as well. :smile: I know he feels there hasn't been much feedback.)

[Jason Rute]

Also, it is good to call out @Chase Norman's Canonical as a very similar tool currently being developed at Carnegie Mellon.

[Chase Norman]

Their tool is not currently capable of proof generation at the level of Canonical.

[Jason Rute]

@Victor Maia :up:

[Srivatsa Srinivas]

@Chase Norman

Does parallel computation benefit proof synthesizers? Whenever I have used an SMT to solve programmatically generated queries (such as exploring a case tree), my queries eventually end up being parallelizable ie, the environment of the queries do not usually depend on each other

[Chase Norman]

Honestly, parallel computation can only benefit by a factor of how many cores you have. When you are operating in such a general complexity class, constant factors are more about latency than capability. Even when there is potential for parallelism, like in SAT, most programs don't bother.