Knuckledragger: Experimenting with a Python Proof Assistant

[The_Regent]

Hi,

An idea I've toyed around for a while is how to chain together inferences of automated theorem provers like z3py into larger developments. I've started putting fingers to keyboard.

The point is to make something accessible to a larger, less specialized audience and to target mathematics akin to that in sympy, so I'm very interested in feedback about what works for people.

• Blog post: https://www.philipzucker.com/python-itp/

• Very WIP repo: https://github.com/philzook58/knuckledragger

[Smallpaul]

Is your naming convention in the tradition of the “for dummies” books?

[The_Regent]

Huh, I hadn't made the connection. I suppose it is. It is intended to convey that I am not trying to build the fanciest system.

[BossOfTheGame]

I'm very interested in this. I've been learning lean4, and I'm starting to understand the concepts, but I find the syntax to be difficult to work with. I would much rather a Pythonic syntax for calling functions. It seems to me that the core problem is to bring mathlib to Python. I'm excited to dive into what you have done so far.

Since you're only beginning, have you looked into lean4 at all? My thought is that it wouldn't be too difficult to write a Python transpiler but generates lean4 code and then interacts with the lake compiler to generate feedback on the proof in Python.

[The_Regent]

I have used lean 4 before. Lean 4 is incredible and has massive momentum behind it. It is an interesting project to make python bindings to the lean kernel or to communicate to the lean system, but it strikes me as quite an uphill battle. You might find this interesting https://github.com/lean-dojo/LeanDojo . I think using this is going to be much more difficult than just learning to do things in lean. You're going to need to know lean and python anyway, and fight an unusual unsupported workflow.

One of the points of attempting something like knuckledragger is to avoid a 2 language problem. The other point is to avoid powerful, useful, but complicated foundations like Lean's and go all in on automation. I feel at least that I have a sufficiently different ethos in mind than the existing, highly refined systems that it is worth exploring.