Commutative Diagram interface to external tools

Stream: general

[Daniel Donnelly]

I'm wanting to at least allow the user to Draw Objects / Arrows (using Quiver - which I have hacked into a mobile (responsive) version) and have this be automatically translated to a single file which defines these objects / arrows in the selected category.

I would then like to automatically put up buttons of theorems that match (I'm sure Lean4 has had some AI facility for this), but not only that, we'll be storing diagrams in a graph database in which we can do monomorphism searches for single diagrams (which either commute or are Noncommutative - might commute), which are then shown to be part of a hypothesis to a proved theorem, which the user can then apply at the click of a button. I know this all sounds exciting and extremely difficult, but just then imagine trying to do all that without Lean4, etc. Seems to me that the most expressive way of doing this would be to piggyback off of Lean4. Yes, I am aware of the InfoView CD Widget.

Can anyone here write me an interface and I will code the rest? Reason I ask is because I would have to learn Lean4 from the basics in order to hack this together. Looking for any guidance as well! :sunglasses:

[Pablo Donato]

this already exists for Coq: https://github.com/dwarfmaster/commutative-diagrams