pith. sign in

arxiv: 2606.01875 · v1 · pith:245TQ2Q4new · submitted 2026-06-01 · 🧮 math.HO · cs.CY

Waterproof Editor: an educational environment for proof assistants and programming languages

Pim Otte , Dick Arends , Raul S\'anchez Flores , Pieter Wils , Jim Portegies This is my paper

Pith reviewed 2026-06-28 11:38 UTC · model grok-4.3

classification 🧮 math.HO cs.CY
keywords Waterproof Editoreducational environmentproof assistantsprogramming languagesnpm packagerich formattinginput areasreuse
0
0 comments X

The pith

Waterproof Editor abstracts rich formatting and input features from Waterproof into an npm package for reuse in teaching proof assistants and programming languages.

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

The paper describes Waterproof Editor, an educational environment derived from the original Waterproof software for teaching mathematical proofs. Its core features, including rich formatting and clear input areas, have been extracted and packaged as a reusable npm component. This package is positioned for integration into varied educational tools focused on proof assistants or programming languages. The authors explicitly invite adoption by others and offer assistance with implementation.

Core claim

Waterproof Editor arose from Waterproof and abstracts its original features such as enabling rich formatting and providing clear input areas into an npm package that can be used in different educational contexts for teaching with proof assistants or programming languages.

What carries the argument

The Waterproof Editor npm package, which isolates and reuses rich formatting and clear input area features for modular integration.

If this is right

  • Educators can add proof assistant support to existing tools by including the package rather than rebuilding input and display logic.
  • The same component supports both mathematical proof teaching and general programming language instruction.
  • New educational projects gain access to the abstracted features without starting from the original Waterproof codebase.
  • The authors' offer of assistance lowers the barrier for adoption in additional contexts.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The package's modularity could allow its input areas to handle proof styles from assistants not used in the original Waterproof development.
  • Widespread reuse might create a de facto standard interface for student proof entry across different tools.
  • Deployment in non-mathematical programming courses would test whether the formatting features transfer beyond proof-specific needs.

Load-bearing premise

The features abstracted from Waterproof are sufficiently modular and general that packaging them as an npm component enables effective reuse without substantial additional engineering in new educational contexts.

What would settle it

A developer attempts to embed the npm package into a new educational tool for a different proof assistant or language and requires substantial custom code changes to make the formatting and input features work.

read the original abstract

Waterproof Editor provides an educational environment specifically targeted to teaching with proof assistants or programming languages. It arose from Waterproof, educational software targeted at helping students acquire the skill of giving mathematical proofs. Its original features such as enabling rich formatting and providing clear input areas are now abstracted away in an npm package and can be used in different educational contexts. We invite interested parties to use this component in their educational software, and offer to assist with this.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The manuscript announces Waterproof Editor, an npm package that extracts core editor features (rich formatting and clear input areas) from the Waterproof educational software for teaching mathematical proofs with proof assistants. It positions the package as reusable across different educational contexts involving proof assistants or programming languages and invites adoption while offering assistance.

Significance. If the reusability claim holds, the package could lower the barrier to building custom educational interfaces for proof assistants by providing pre-built components for formatting and input. However, the manuscript contains no usage examples, API documentation, integration case studies, or verification of modularity, so the significance remains potential rather than demonstrated.

major comments (1)
  1. Abstract: The central claim that the original features 'are now abstracted away in an npm package and can be used in different educational contexts' is presented without any concrete description of the package API, installation instructions, or even a minimal usage example, leaving the reusability assertion unsupported.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. The manuscript is a short announcement of the npm package, and we agree that it does not currently provide concrete API details or examples to support the reusability claim. We will revise accordingly.

read point-by-point responses

  1. Referee: Abstract: The central claim that the original features 'are now abstracted away in an npm package and can be used in different educational contexts' is presented without any concrete description of the package API, installation instructions, or even a minimal usage example, leaving the reusability assertion unsupported.

    Authors: We agree that the current text provides no API description, installation instructions, or usage example, leaving the reusability claim unsupported by concrete evidence in the manuscript. The paper was prepared as a brief announcement to alert the community to the package's availability and our willingness to assist with integration. In the revised version we will add a short section containing npm installation instructions, a high-level description of the exported components, and a minimal self-contained usage example. revision: yes

Circularity Check

0 steps flagged

No circularity; descriptive software announcement with no derivations or self-referential claims

full rationale

The manuscript is a short announcement of an npm package extracted from Waterproof. It contains no equations, no fitted parameters, no predictions, no uniqueness theorems, and no load-bearing citations. The central statement—that features have been abstracted into a reusable component—is a factual description of engineering work, not a derivation that reduces to its own inputs by construction. No patterns from the enumerated circularity kinds apply.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is a software tool description paper with no mathematical claims, derivations, or empirical results, so the ledger contains no entries.

pith-pipeline@v0.9.1-grok · 5602 in / 1031 out tokens · 23229 ms · 2026-06-28T11:38:41.481012+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

9 extracted references · 5 canonical work pages

  1. [1]

    jscoq: Towards hybrid theorem proving interfaces

    Emilio Jes \'u s Gallego Arias, Beno \^ t Pin, and Pierre Jouvelot. jscoq: Towards hybrid theorem proving interfaces. arXiv preprint arXiv:1701.07125 , 2017

    Pith/arXiv arXiv 2017

  2. [2]

    Number theory and axiomatic geometry in the D iproche system

    Merlin Carl. Number theory and axiomatic geometry in the D iproche system. Electronic Proceedings in Theoretical Computer Science , 328:56–78, October 2020. URL: http://dx.doi.org/10.4204/EPTCS.328.4, https://doi.org/10.4204/eptcs.328.4 doi:10.4204/eptcs.328.4

    work page doi:10.4204/eptcs.328.4 2020

  3. [3]

    Jupyter notebooks - a publishing format for reproducible computational workflows

    Thomas Kluyver, Benjamin Ragan-Kelley, Fernando P \'e rez, Brian Granger, Matthias Bussonnier, Jonathan Frederic, Kyle Kelley, Jessica Hamrick, Jason Grout, Sylvain Corlay, Paul Ivanov, Dami \'a n Avila, Safia Abdalla, Carol Willing, and Jupyter development team. Jupyter notebooks - a publishing format for reproducible computational workflows. In Fernando...

    2016

  4. [4]

    Teaching Mathematics Using Lean and Controlled Natural Language

    Patrick Massot. Teaching Mathematics Using Lean and Controlled Natural Language . In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving (ITP 2024) , volume 309 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 27:1--27:19, Dagstuhl, Germany, 2024. Schloss Dagstuhl -- Lei...

    work page doi:10.4230/lipics.itp.2024.27 2024

  5. [5]

    Untangling mechanized proofs

    Cl\' e ment Pit-Claudel. Untangling mechanized proofs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering , SLE 2020, page 155–174, New York, NY, USA, 2020. Association for Computing Machinery. https://doi.org/10.1145/3426425.3426940 doi:10.1145/3426425.3426940

    work page doi:10.1145/3426425.3426940 2020

  6. [6]

    Waterproof: Transforming a proof assistant into an educational tool

    Jim Portegies, Jelle Wemmenhove, Pim Otte, and Dick Arends. Waterproof: Transforming a proof assistant into an educational tool. Nieuw Archief van de Wiskunde , 26:212--214, December 2025

    2025

  7. [7]

    Waterproof: Educational software for learning how to write mathematical proofs

    Jelle Wemmenhove, Dick Arends, Thijs Beurskens, Maitreyee Bhaid, Sean McCarren, Jan Moraal, Diego Rivera Garrido, David Tuin, Malcolm Vassallo, Pieter Wils, and Jim Portegies. Waterproof: Educational software for learning how to write mathematical proofs. Electronic Proceedings in Theoretical Computer Science , 400:96–119, April 2024. URL: http://dx.doi.o...

    work page doi:10.4204/eptcs.400.7 2024

  8. [8]

    Service design for the improvement of intelligent tutoring systems: A case study

    Jelle Wemmenhove, Dorina Bór, Rianne Conijn, and Jim Portegies. Service design for the improvement of intelligent tutoring systems: A case study. Journal of Computer Assisted Learning , 41(4):e70088, 2025. e70088 JCAL-24-1207.R1. URL: https://onlinelibrary.wiley.com/doi/abs/10.1111/jcal.70088, https://arxiv.org/abs/https://onlinelibrary.wiley.com/doi/pdf/...

    work page doi:10.1111/jcal.70088 2025

  9. [9]

    Comparative analysis of student proof structure following the use of waterproof

    Jelle Wemmenhove, Nick Hoofd, Alexander Schüler-Meyer, and Jim Portegies. Comparative analysis of student proof structure following the use of waterproof. To appear in post-proceedings of ThEdu 25, 2026

    2026