English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

In proof assistants, the physical proximity between two formal mathematicalconcepts is a strong predictor of their mutual relevance. Furthermore, lemmaswith close proximity regularly exhibit similar proof structures. We show thatthis locality property can be exploited through online learning techniques toobtain solving agents that far surpass offline learners when asked to provetheorems in an unseen mathematical setting. We extensively benchmark two suchonline solvers implemented in the Tactician platform for the Coq proofassistant: First, Tactician's online $k$-nearest neighbor solver, which canlearn from recent proofs, shows a $1.72\times$ improvement in theorems provedover an offline equivalent. Second, we introduce a graph neural network,Graph2Tac, with a novel approach to build hierarchical representations for newdefinitions. Graph2Tac's online definition task realizes a $1.5\times$improvement in theorems solved over an offline baseline. The $k$-NN andGraph2Tac solvers rely on orthogonal online data, making them highlycomplementary. Their combination improves $1.27\times$ over their individualperformances. Both solvers outperform all other general-purpose provers forCoq, including CoqHammer, Proverbot9001, and a transformer baseline by at least$1.48\times$ and are available for practical use by end-users.

Graph2Tac: Online Representation Learning of Formal Math Concepts