[philzook]

It's interesting how sometimes it feels like a topic starts showing up super often all of the sudden. It probably isn't a coincidence, since my interest and probably this post's interest is due to Tao's recent equation challenge https://teorth.github.io/equational_theories/ .

I was surprised and intrigued to find Wolfram's name when I was reading background literature doing this blog post https://www.philipzucker.com/cody_sheffer/ where I translated my friend's Lean proof of the correspondence of Sheffer stroke to Boolean algebra in my python proof assistant knuckledragger https://github.com/philzook58/knuckledragger (an easier result than Wolfram's single axiom one).

I was also intrigued reading about the equational theorem prover Waldmeister https://www.mpi-inf.mpg.de/departments/automation-of-logic/s... that it may have been acquired by Mathematica? It's hard to know how Mathematica's equational reasoning system is powered behind the scenes.

Mathematica can really make for some stunning visuals. Quite impressive.