Pith. sign in

REVIEW 1 major objections 5 minor 25 references

Exploring Formal Math on the Blockchain: An Explorer for Proofgold

T0 review · 1 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A web-based explorer for the Proofgold blockchain makes the formal mathematics embedded in the chain — theories, definitions, theorems, proofs, and bounties — browsable and interactive, demonstrated on 33 category-theory adjunction conjectu

desk verdict A real, working explorer for Proofgold with a solid case study; the reorg/cache question is legitimate but minor, and the paper deserves peer review. read the letter →

arxiv 2509.08267 v1 pith:ETJEAMW6 submitted 2025-09-10 cs.LO

Chad E. Brown , Cezary Kaliszyk , Josef Urban This is my paper
classification cs.LO MSC 03B1518A40
keywords blockchainexplorerformalizedmathematicsProofgoldproofcheckingintuitionistichigher-orderlogicadjointfunctorscategorytheorybounties
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper presents a web-based explorer for Proofgold, a blockchain that records formalized mathematics — theories, definitions, propositions, proofs, and proof bounties — alongside cryptocurrency transactions. Until now Proofgold was usable only through a 210-command command-line client, so the explorer's claim is that the formal mathematical content buried in the chain can be surfaced in a browsable, interactive web interface without lowering trust in the chain's verdicts. The system caches structured data about every formal object in memory (34 hashtables, about 10 gigabytes, refreshed hourly) and serves it through a PHP backend with a custom RPC layer. To show this works for real mathematics, the authors run a case study of 33 bounty-backed conjectures asserting the existence of left adjoints to forgetful functors in category theory, of which 14 had been resolved by May 2025 — including a disproven conjecture that exposed a definitional bug in the formalization of monoids.

What carries the argument

The load-bearing mechanism is the explorer-mode extension of the Proofgold Lava client: thirty-four OCaml hashtables that precompute and hold roughly ten gigabytes of structured metadata about every formal object on the chain, refreshed hourly, so that lookups of theories, definitions, proofs, owners, dependencies, and bounty histories do not require re-traversing the whole ledger. The formal side of the argument is carried by the case-study machinery: the HOTG set-theory encoding of category theory given by the predicates MetaCat, MetaFunctor, MetaNatTrans, and MetaAdjunction_strict — the last asserting that two explicitly supplied functors and two natural transformations form an adjunction

What would settle it

Take a sample of the on-chain proof documents the explorer displays as 'proven' and re-check them with an independent implementation of the same logic (intuitionistic higher-order logic with functional extensionality); if any accepted document fails the independent check, the explorer's status display is not trustworthy. A cheaper test: submit a deliberately flawed proof document through the explorer's transaction interface and see whether the chain rejects it before it can appear as 'proven.'

Watch

Extended reading notes

Core claim

The paper's central claim is that the explorer it built — extending the Proofgold Lava client with an 'explorer mode' that precomputes and caches structured information about the chain's formal content — gives users efficient, structured access to theories, definitions, theorems, proofs, and bounties, and supports light interaction such as submitting signed transactions. The cached indexes (34 OCaml hashtables holding roughly 10 gigabytes, refreshed hourly) turn an unwieldy full-history traversal into fast lookups of formal entities, their owners, dependencies, and bounty status, served to a PHP front end over a custom RPC layer. The paper further claims this infrastructure supports a practi

Load-bearing premise

The Proofgold proof checker for intuitionistic higher-order logic is sound and correctly implemented; the explorer only relays the chain's proven/disproven verdicts, and the paper provides no independent verification of that checker, so a checker bug would make the displayed statuses and the case-study conclusions unreliable.

Editorial extensions

If this is right

  • Formal knowledge on Proofgold becomes inspectable by anyone with a browser, so results such as the 12 of Wiedijk's 100 theorems proved in Megalodon can be read and built upon without running a node or learning the CLI.
  • Proof bounties become a visible marketplace: users can see the highest open and collected bounties and focus effort on valuable open conjectures such as the free-group adjunction.
  • The chain graph's coloring of theory-defining, proof-carrying, and bounty-carrying nodes, plus its marking of invalid or missing nodes, gives a public audit view of both the ledger and the quality of the formal content in it.
  • The Megalodon Wiki integration creates an end-to-end pipeline from a collaboratively edited formal file to an on-chain, bounty-bearing proof document.
  • The case study demonstrates that bounty-backed conjectures can drive real mathematical findings, including a refutation that revealed a definitional bug in the formal category of monoids (semigroup homomorphisms that need not preserve identity).

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If this explorer becomes the standard gateway, the practical trust question shifts from data access to the soundness of the on-chain checker itself: users will read 'proven' and 'disproven' as ground truth, so an independent audit of the Proofgold checker becomes the natural next stress test.
  • The 19 still-open adjoint conjectures constitute a public, bountied benchmark suite for automated theorem proving; they could be used to compare proof-finding and formalization automation in a way that standard libraries cannot, because the attached rewards create a measurable incentive.
  • The architecture generalizes: any append-only repository of structured mathematical content could receive the same treatment of precomputed offline indexes plus a web front end, making the explorer a template for mathematical knowledge management beyond blockchains.
  • The monoid refutation suggests a testable hypothesis about incentive design: bounty systems can serve as a distributed bug-finding mechanism for formal libraries, which would be a new argument for attaching rewards to conjectures in centralized repositories too.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper presents a web-based blockchain explorer for Proofgold, a blockchain that stores formal mathematical content. The authors describe the system architecture: a modified Proofgold Lava client in a new 'explorer mode' that caches structured information about formal objects, a PHP backend, and an RPC layer. The explorer supports viewing blocks, transactions, addresses, theories, definitions, proofs, bounties, and the chain graph, and it includes a transaction submission interface. The paper also presents a case study of 33 adjunction conjectures in category theory formalized in Proofgold's HOTG theory, reporting which are proven, disproven, or open, and discussing two examples in detail. The paper claims the explorer provides accessible, structured access to formal mathematical content on the blockchain.

Significance. If the described system works as claimed, it is a useful contribution to the infrastructure for decentralized formal mathematics. The explorer lowers the barrier to Proofgold, which was previously CLI-only, and integrates with the Megalodon Wiki. The case-study results are backed by machine-checked proofs processed by the Proofgold proof checker, and the paper gives live URLs and screenshots. The paper does not claim to verify the proof checker itself, which is appropriate for a system description. The formalization of category theory and the discussion of the monoid 'bug' are interesting concrete illustrations. Overall, this is a relevant systems paper for the formal mathematics / blockchain community.

major comments (1)
  1. [Section 3 and Section 5 (Table 1)] The caching layer is described as 'periodically (every hour) refreshed' and stored in 34 OCaml hashtables, but the paper never states which chain tip the cache follows or how reorganizations are processed. This matters because Figure 3 shows competing chain tips, and the explorer displays 'proven', 'disproven', 'collected', and 'open' statuses that Table 1 relies on. If the cache is built from a branch that is later orphaned, the displayed statuses are stale or indefinitely wrong unless reorg handling is specified. Please add an explicit statement of the canonical-chain selection policy and how the hourly refresh interacts with chain reorganizations (e.g., the cache is rebuilt from the current best chain).
minor comments (5)
  1. [Section 5] In the description of the functor F1, 'the arrow from F0 X to F1 Y' should presumably be 'the arrow from F0 X to F0 Y' (f: X -> Y should map to D(F0 X, F0 Y)).
  2. [Section 4] Typo: 'conejctures' should be 'conjectures' in the paragraph about bounty categories.
  3. [Figure 3] The chain graph includes node labels such as 'qf8mw' and 'qn76a' that are not explained in the caption. A brief explanation in the caption or text would improve readability.
  4. [Throughout] The spelling 'Groethendieck' appears in Figures and text; the standard spelling is 'Grothendieck'.
  5. [Section 3] The paper describes the modified Lava client and PHP backend but does not provide a repository link for the source code. Adding such a link would aid reproducibility for other researchers.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the explorer's functionality is documented as a live system and the formalization statuses are outputs of an independent proof checker, not consequences of the paper's own assumptions.

full rationale

The paper's central contribution is a web-based blockchain explorer for Proofgold. Its claims are about the existence and behavior of a software system, supported by architecture descriptions, screenshots, and a live deployment (Section 3–4). The case study (Section 5) presents 33 conjectures with statuses (proven/disproven/open) obtained from the Proofgold blockchain, where the status is determined by the Proofgold proof checker—an implementation described in prior work [8] by overlapping authors. This is a real external check, not a self-fulfilling prediction: the checker itself is not formally verified, but the paper does not claim to derive the statuses from the checker's correctness; it merely reports what the checker says. No parameter is fitted, no uniqueness theorem is invoked to force a choice, and no known result is merely renamed. The self-citations to Proofgold [8] and HOTG [9] provide background and infrastructure, but they are not load-bearing in the sense that the explorer's utility or the formalization outcomes reduce to those citations by construction. The only substantive assumption—soundness of the proof checker—is an external trust boundary, not a circular step. Thus the paper is essentially self-contained for its claims, and any concerns about reorg handling or cache staleness are correctness risks, not circularity.

Assumptions & free parameters 0 free parameters · 1 assumptions · 0 invented entities

The paper introduces no free parameters or newly invented mathematical entities; it relies on the previously published HOTG theory and the Proofgold infrastructure.

assumptions (1)
  • domain assumption HOTG axioms (Tarski-Grothendieck set theory) and the proof-checking rules of intuitionistic higher-order logic
    The case-study formalizations in Section 5 build on the HOTG theory axiomatized in prior work [9]; the paper's claims about proven/disproven statuses depend on these axioms and the soundness of the proof checker.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Exploring Formal Math on the Blockchain: An Explorer for Proofgold." pith.science (2026). https://pith.science/paper/ETJEAMW6

@misc{pith2026250908267,
  author       = {Pith},
  title        = {Pith review of: Exploring Formal Math on the Blockchain: An Explorer for Proofgold},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ETJEAMW6}},
  note         = {Machine review of arXiv:2509.08267}
}
read the original abstract

Proofgold is a blockchain that supports formalized mathematics alongside standard cryptocurrency functionality. It incorporates logical constructs into the blockchain, including declarations of formal theories, definitions, propositions and proofs. It also supports placing and collecting bounties on proving these propositions, incentivizing the development of the formal libraries contained in Proofgold. In this paper, we present a web-based blockchain explorer for Proofgold. The system exposes not only the usual transactional data but also the formal mathematical components embedded in the chain and allows some interaction with them. The explorer allows users to inspect blocks, transactions, and addresses, as well as formal objects: theories, definitions, theorems and their proofs. We also support the submission of transactions to the blockchain using our interface. We describe the system architecture and its integration with the Proofgold Lava software, highlighting how the explorer supports navigation of formal content and facilitates mathematical knowledge management in a decentralized setting, as well as a number of formalizations in category theory done in the system.

Figures

Figures reproduced from arXiv: 2509.08267 by the authors.

Figure 1
Figure 1. High-level architecture of the explorer blocks. Additionally, two theories axiomatizing HOTG have been published [9], one corresponding to Mizar [4] and one corresponding to Megalodon, along with a theory for reasoning about syntax using higher-order abstract syntax (HOAS). These theories have facilitated the formalization of various mathematical con￾cepts and the construction of significant mathematical objects, su… view at source ↗
Figure 2
Figure 2. Explorer Main Page In explorer mode, the Lava client computes and caches additional informa￾tion about the formal content embedded in the blockchain. This includes the possibility of looking up definitions, propositions, theories, proofs and boun￾ties. In principle, this information is already stored in the blockchain, but it requires traversing the whole history. The added information is stored in 34 OCaml hashtabl… view at source ↗
Figure 3
Figure 3. Chain Graph The explorer is also connected to the Megalodon Wiki (mgwiki)3 which is a collaborative git-based platform for for￾mal math that enables users to edit and verify Megalodon files directly in the browser. The mgwiki workflow involves cloning or forking the repository, modi￾fying or adding .mg files, and commit￾ting changes, which triggers automated proof checking and HTML generation via GitHub Actions. Err… view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Highest open and collected bounties Bounties Open Collected Mizar Random A MI Surreal OEIS AbstrHF QBF [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Open and collected bounty categories the blockchain. This is normally a single chain with branches in the case of com￾peting chain tips. We show an example from a time when there were multiple competing nodes ( [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: Fermat as a bounty in the Proofgold explorer and its corresponding statement in the Megalodon Wiki valuable open conjectures and focus their proof efforts on them, as well as to see what are the domains of the conejctures users are working on. The individual bounties c…
Figure 7
Figure 7. Figure 7: Explorer view of a block [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]
Figure 8
Figure 8. Figure 8: Explorer view of a transaction. Clicking “. . . ” allows inspecting the proof. 5 Use Case and Examples Some of the examples of conjectures with bounties – many of which have already been proven or disproven – assert the existence of a left adjoint to a forgetful [PITH…
Figure 9
Figure 9. Figure 9: The higher-order Tarski Groethendieck theory in the explorer functor. Such left adjoints, when they exist, often correspond to freely generated structures. More generally, the interest in such adjoints can be justified by Slogan IV of [19]: “Many important concepts in …
Figure 10
Figure 10. Figure 10: Definitions for the Adjoint Functor for Bijections in the Megalodon Wiki [PITH_FULL_IMAGE:figures/full_fig_p014_10.png]
Figure 12
Figure 12. Figure 12: The most recent of the 33 propositions to be disproven takes D to be a category with monoids as objects. Here “disproven” means the negation of the proposition was proven. This should be surprising as it is clear that given a set X one can create a monoid freely gener…
Figure 12
Figure 12. Figure 12: Existential Adjunction Theorem for Bijections in the Megalodon Wiki [PITH_FULL_IMAGE:figures/full_fig_p015_12.png]
Figure 14
Figure 14. Figure 14: There is no Left Adjoint to the Forgetful Functor for Monoids in the Mega￾lodon Wiki why the existential assumption can be “applied” to the current goal (of proving ⊥), followed by a “let” (essentially giving a fresh name x for the object) and an “assume” (giving the …

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

25 extracted references · 18 canonical work pages

  1. [1]

    CoRRabs/1910.09336(2019),http://arxiv

    The Lean mathematical library. CoRRabs/1910.09336(2019),http://arxiv. org/abs/1910.09336

    arXiv 1910

  2. [2]

    Ahrens, B., Matthes, R., Mörtberg, A.: From signatures to monads in Uni- Math. J. Autom. Reason.63(2), 285–318 (2019).https://doi.org/10.1007/ S10817-018-9474-4,https://doi.org/10.1007/s10817-018-9474-4

    work page doi:10.1007/s10817-018-9474-4 2019

  3. [3]

    In: Filliâtre, J., Paulin-Mohring, C., Werner, B

    Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based math- ematical search engine: Whelp. In: Filliâtre, J., Paulin-Mohring, C., Werner, B. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3839, p...

    work page doi:10.1007/11617990_2 2004

  4. [4]

    Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K.: The role of the Mizar mathematical library for interactive proof development in Mizar. J. Autom. Reason.61(1-4), 9– 32 (2018).https://doi.org/10.1007/S10817-017-9440-6,https://doi.org/ 10.1007/s10817-017-9440-6

    doi:10.1007/s10817-017-9440-6 2018

  5. [5]

    In: Kaliszyk, C., Brady, E.C., Kohlhase, A., Coen, C.S

    Bercic, K., Kohlhase, M., Rabe, F.: Towards a unified mathematical data in- frastructure: Database and interface generation. In: Kaliszyk, C., Brady, E.C., Kohlhase, A., Coen, C.S. (eds.) Intelligent Computer Mathematics - 12th Interna- tional Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Pro- ceedings. Lecture Notes in Computer Science,...

    work page doi:10.1007/978-3-030-23250-4_3 2019

  6. [6]

    In: Murray, T.C., Stefan, D

    Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella- Béguelin, S.: Formal verification of smart contracts: Short paper. In: Murray, T.C., Stefan, D. (eds.) Proceedings of the 2016 ACM Workshop on Programming Lan- guages and Analysis for Security, PLAS@C...

    work page arXiv 2016

  7. [7]

    In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V

    Blanchette, J.C., Haslbeck, M.W., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. Lecture Notes in Com- puter Science, vol. 9150, pp. 3–17. Springer...

    work page doi:10.1007/978-3-319-20615-8_1 2015

  8. [8]

    In: Dargaye, Z., Schneidewind, C

    Brown, C.E., Kaliszyk, C., Gauthier, T., Urban, J.: Proofgold: Blockchain for for- mal methods. In: Dargaye, Z., Schneidewind, C. (eds.) 4th International Work- shop on Formal Methods for Blockchains, FMBC@CAV 2022, August 11, 2022, Haifa, Israel. OASIcs, vol. 105, pp. 4:1–4:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022).https://doi.org/10.4...

    work page doi:10.4230/oasics.fmbc.2022.4 2022

Show all 25 references
  1. [9]

    In: Kaliszyk, C., Brady, E.C., Kohlhase, A., Coen, C.S

    Brown, C.E., Pąk, K.: A tale of two set theories. In: Kaliszyk, C., Brady, E.C., Kohlhase, A., Coen, C.S. (eds.) Intelligent Computer Mathematics - 12th Interna- tional Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Pro- ceedings. Lecture Notes in Computer Sci...

    2019 doi

  2. [10]

    In: Blanchette, J., Hritcu, C

    Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN Inter- national Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. pp. 299–312. ACM (20...

    2020

  3. [11]

    Formalized Mathematics 1(2), 409–420 (1990),http://fm.mizar.org/1990-1/pdf1-2/cat_1.pdf

    Byliński, C.: Introduction to categories and functors. Formalized Mathematics 1(2), 409–420 (1990),http://fm.mizar.org/1990-1/pdf1-2/cat_1.pdf

    1990

  4. [12]

    In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W

    Corbineau, P., Kaliszyk, C.: Cooperative repositories for formal proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Towards Mecha- nized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th Interna- tional Conference, MKM 2007, Hagenberg, Austria, J...

    2007 doi

  5. [13]

    In: Bertot, Y., Kutsia, T., Norrish, M.(eds.)15thInternationalConferenceonInteractiveTheoremProving,ITP2024, September 9-14, 2024, Tbilisi, Georgia

    Desharnais, M., Tóth, B., Waldmann, U., Blanchette, J., Tourret, S.: A modular formalization of superposition in Isabelle/HOL. In: Bertot, Y., Kutsia, T., Norrish, M.(eds.)15thInternationalConferenceonInteractiveTheoremProving,ITP2024, September 9-14, 2024, Tbilisi, Georgia. L...

    2024 doi

  6. [14]

    In: Kiselyov, O

    Doan, T.T.H., Thiemann, P.: A formal verification framework for tezos smart con- tracts based on symbolic execution. In: Kiselyov, O. (ed.) Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22- 24, 2024, Proceedings. Lecture Notes in C...

    2024

  7. [15]

    In: Buzzard, K., Kut- sia, T

    Furushima, H., Yamamichi, D., Shigenaka, S., Nakasho, K., Wasaki, K.: An in- tegrated web platform for the Mizar mathematical library. In: Buzzard, K., Kut- sia, T. (eds.) Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September ...

    2022 doi

  8. [16]

    In: Blazy, S., Paulin-Mohring, C., Pichardie, D

    Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Picha...

    2013

  9. [17]

    Forum of Mathematics, Pi5(2017).https://doi.org/10.1017/fmp.2017.1

    Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso,J.,Rute,J.,Solovyev,A.,Ta,T.H.A.,Tran,N.T.,Trieu,T.D.,Urban,J.,Vu, K., Zumkeller, R.: A formal proof of the...

    2017 doi

  10. [18]

    Acta Didactica Napocensia3(2), 35–48 (June 2010) 20 C

    Hendriks, M., Kaliszyk, C., van Raamsdonk, F., Wiedijk, F.: Teaching logic using a state-of-the-art proof assistant. Acta Didactica Napocensia3(2), 35–48 (June 2010) 20 C. Brown, C. Kaliszyk, J. Urban

    2010

  11. [19]

    Cambridge University Press, Cambridge, UK (1986)

    Lambek, J., Scott, P.: Introduction to higher order categorical logic. Cambridge University Press, Cambridge, UK (1986)

    1986

  12. [20]

    In: Naumowicz, A., Thiemann, R

    Nawrocki, W., Ayers, E.W., Ebner, G.: An extensible user interface for Lean 4. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on In- teractive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland. LIPIcs, vol. 268, pp. 24:1–24:20. Schlo...

    2023 doi

  13. [21]

    Stark, E.W.: Category theory with adjunctions and limits. Arch. Formal Proofs 2016(2016),https://www.isa-afp.org/entries/Category3.shtml

    2016

  14. [22]

    Sci Data10(791) (2023),https: //doi.org/10.1038/s41597-023-02681-3

    Tomaszuk, D., Szeremeta, Ł., Korniłowicz, A.: MMLKG: Knowledge graph for mathematical definitions, statements and proofs. Sci Data10(791) (2023),https: //doi.org/10.1038/s41597-023-02681-3

    2023 doi

  15. [23]

    Vezzosi, A., Mörtberg, A., Abel, A.: Cubical Agda: a dependently typed pro- gramming language with univalence and higher inductive types. Proc. ACM Program. Lang.3(ICFP), 87:1–87:29 (2019).https://doi.org/10.1145/3341691, https://doi.org/10.1145/3341691

    2019 doi

  16. [24]

    In: Wiedijk, F

    Wiedijk, F.: Introduction. In: Wiedijk, F. (ed.) The Seventeen Provers of the World, Foreword by Dana S. Scott, Lecture Notes in Computer Science, vol. 3600, pp. 1–9. Springer (2006).https://doi.org/10.1007/11542384_1,https://doi. org/10.1007/11542384_1

    2006 doi

  17. [324]

    Springer (2024).https://doi.org/10.1007/978-981-97-8943-6_15,https: //doi.org/10.1007/978-981-97-8943-6_15

    2024 doi

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.