First impression and thoughts

[zhtprog]

I have tried out the vscode extension. I think it is a cool idea and it could develop into something interesting.

Do you have any experience with dependent type based proof assistants such as the Lean prover or Coq? One nice thing about these is the type based accurate dynamic auto completion. In addition to assistance in recall it also ensures type correctness. Of course these provers are geared towards verification instead of authoring so we typically associate them with painstakingly baby steps in proof construction. But if the type feature is extracted for the purpose of authoring semantic math databases it could be a different story.

I think the database approach holds promise as there is quality in quantity, as is the ethos of the ML world. One way quantity could help is when more entries in one area have been created, creating new entries becomes less laborious with the tooling offering more and more precise feedback. The positive feedback loop is important if accumulation of entries will mostly be done by hand.

A type based prover tends to have a sound logic framework that is semantically unambiguous. Of course the precision of type theory can be a onerous straitjacket as well. It could make many things hard to say. Maybe syntactic patterns suffice at times -- which makes the database easier to construct and curate. Still it would be nice to have a core fragment be as precisely defined as possible, which in the long term enhances the precision of query answering (and thus providing more useful feedback in aiding its own construction as well). It would be interesting to see where the right balance is.

I hope these thoughts are of interest to you.

Haitao

[domini...@gmail.com]

Thanks for the feedback.  I find it really helpful.  I'm looking into having MathLingua be backed by a formal theorem proving system.  However, as you said such a system requires strict conformance to the way things are represented in the system.

I like your idea of having a core part of definitions that are formally defined, with other parts that are less formal, but can be made to be more formal as time progresses.  This follows the overall form of MathLingua to be flexible in its design.

I don't have a lot of experience in proof assistants beyond theoretical aspects of dependent type theory.  In particular, I am not sure which proof assistant/system I should use to back MathLingua.  Right now I'm thinking Lean might be the way to go.  Do you have a preference for a theorem prover that stands out for you?

Thanks

Dominic