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

The Agora system is a prototype "Wiki for Formal Mathematics", with an aim tosupport developing and documenting large formalizations of mathematics in aproof assistant. The functions implemented in Agora include in-browser editing,strong AI/ATP proof advice, verification, and HTML rendering. The HTMLrendering contains hyperlinks and provides on-demand explanation of the proofstate for each proof step. In the present paper we show the prototype FlyspeckWiki as an instance of Agora for HOL Light formalizations. The wiki can be usedfor formalizations of mathematics and for writing informal wiki pages aboutmathematics. Such informal pages may contain islands of formal text, which isused here for providing an initial cross-linking between Hales's informalFlyspeck book, and the formal Flyspeck development.  The Agora platform intends to address distributed wiki-style collaboration onlarge formalization projects, in particular both the aspect of immediateediting, verification and rendering of formal code, and the aspect of gradualand mutual refactoring and correspondence of the initial informal text and itsformalization. Here, we highlight these features within the Flyspeck Wiki.

Formal Mathematics on Display: A Wiki for Flyspeck