VictorTaelin: SupGen is a coding AI runs on 1 core CPU can prove theorems (twitter.com) 38 points by hyperbrainer 1y ago ↗ HN
[–] software-is-art 1y ago ↗ Reminds me of miniKanren but with static typing (which I’ve always wanted to see an implementation of).Will be playing with the various releases of SupGen as you improve it
[–] sw1sh 1y ago ↗ This is very cool! I'm wondering how does it compare to classical ATPs like Waldmeister or Vampire, can SupGen compete in CASC (https://tptp.org/CASC/)?For example, can it proof this example from the recent Stephen Wolfram's post https://writings.stephenwolfram.com/2025/01/who-can-understa... ? Which is basically about proving a•b=b•a from a single axiom ((a•b)•c)•(a•((a•c)•a))=c.Is the source code available for this btw?
6 comments
[ 2.9 ms ] story [ 27.3 ms ] threadWill be playing with the various releases of SupGen as you improve it
For example, can it proof this example from the recent Stephen Wolfram's post https://writings.stephenwolfram.com/2025/01/who-can-understa... ? Which is basically about proving a•b=b•a from a single axiom ((a•b)•c)•(a•((a•c)•a))=c.
Is the source code available for this btw?