I'm working on Knuckledragger, a proof assistant shallowly based upon z3py https://github.com/philzook58/knuckledragger

Yesterday I proved the infinitude of primes, which I was pretty happy with. https://www.philipzucker.com/knuckle_primes/ A trivial theorem in the scheme of things, but one for which z3 certainly can't do it on it's own.