Automated theorem proving with (deep) reinforcement learning (DRL) approach is hot topic in current AI research when domains of games are becoming saturated and completed research topics. For example, there is a path from automated mathematics towards AGI as sketched by the workshop https://mathai-iclr.github.io/

DRL automated theorem proving essentially is the exploration of the state space in which each state is labelled by formulas for

  1. current (sub)goals that should be proved (current proof obligations);

  2. set of currently proved facts (lemmas).

Essentially - each state is set of unproved and proved formulas.

Mathematical expressions can be encoded in different ways - e.g. by lambda terms (Coq), by expressions in higher order logic (Isabelle/HOL), but Mizar, Lean, etc expressions.

To do such exploration of state space in which each state is labelled by formulas, one should be able to have engineered feature of such formulas of engineer such featured automatically (online, on the fly manner).

My question is - what are those features? Are there any research work that researches such features, be they neural or symbolic? Essentially, it could be the "mathematics of mathematical expressions (which capture both syntax and semantics in somewhat meaningful balance)"?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.