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/

Global: Zendy Plus annual

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

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Humans prove theorems by relying on substantial high-level reasoning andproblem-specific insights. Proof assistants offer a formalism that resembleshuman mathematical reasoning, representing theorems in higher-order logic andproofs as high-level tactics. However, human experts have to construct proofsmanually by entering tactics into the proof assistant. In this paper, we studythe problem of using machine learning to automate the interaction with proofassistants. We construct CoqGym, a large-scale dataset and learning environmentcontaining 71K human-written proofs from 123 projects developed with the Coqproof assistant. We develop ASTactic, a deep learning-based model thatgenerates tactics as programs in the form of abstract syntax trees (ASTs).Experiments show that ASTactic trained on CoqGym can generate effective tacticsand can be used to prove new theorems not previously provable by automatedmethods. Code is available at https://github.com/princeton-vl/CoqGym.

Learning to Prove Theorems via Interacting with Proof Assistants