Skip to content

@impermeable impermeable

Change the repository type filter

All

    Repositories list

    28 repositories

    • rocq-waterproof

      Public
      The Waterproof plugin for the Rocq proof assistant allows you to write Rocq proofs in a style that resembles handwritten mathematical proofs, designed to help u…
      Rocq Prover
      •
      GNU Lesser General Public License v3.0
      •19•51•24•3•Updated Aug 24, 2026Aug 24, 2026

    • waterproof-vscode

      Public
      TypeScript
      •
      GNU Lesser General Public License v2.1
      •6•12•35•4•Updated Aug 23, 2026Aug 23, 2026

    • waterproof-editor

      Public
      Editor used in the Waterproof project.
      TypeScript
      •
      MIT License
      •1•4•16•5•Updated Aug 23, 2026Aug 23, 2026

    • introduction-to-proof-sheets-lean

      Public
      Lean
      •
      Other
      •0•1•0•0•Updated Aug 20, 2026Aug 20, 2026

    • impermeable.github.io

      Public
      HTML
      •0•0•0•0•Updated Aug 20, 2026Aug 20, 2026

    • verbose-lean4

      Public
      Natural language tactics to teach mathematics using Lean 4
      Lean
      •
      Apache License 2.0
      •24•0•0•0•Updated Aug 12, 2026Aug 12, 2026

    • waterproof-javascript

      Public
      Learn JavaScript using Waterproof!
      TypeScript
      •
      MIT License
      •0•0•0•0•Updated Jul 24, 2026Jul 24, 2026

    • waterproof-river

      Public
      AI assistant for the Waterproof vscode extension
      TypeScript
      •
      MIT License
      •0•0•1•0•Updated Jul 24, 2026Jul 24, 2026

    • waterproof-genre

      Public
      Lean
      •
      MIT License
      •2•0•1•1•Updated Jul 24, 2026Jul 24, 2026

    • aquarium

      Public
      Standalone version of Waterproof that runs fully within the webbrowser
      TypeScript
      •0•1•4•0•Updated Jul 23, 2026Jul 23, 2026

    • codemirror-lang-waterproof

      Public
      CodeMirror language package for Waterproof support
      TypeScript
      •
      MIT License
      •0•0•0•0•Updated Jul 16, 2026Jul 16, 2026

    • codemirror-lang-verbose

      Public
      CodeMirror language package for Verbose Lean support
      TypeScript
      •
      MIT License
      •1•0•0•0•Updated Jul 13, 2026Jul 13, 2026

    • YalepSheets

      Public
      Lean
      •
      GNU General Public License v3.0
      •0•0•0•0•Updated Jul 1, 2026Jul 1, 2026

    • waterproof-exercise-sheets

      Public
      Examples of Waterproof exercise sheets used for teaching Analysis 1 at the TU/e.
      GNU Lesser General Public License v2.1
      •4•3•0•1•Updated Apr 9, 2026Apr 9, 2026

    • waterproof

      Public archive
      Waterproof is an educational environment for writing mathematical proofs in interactive notebooks. See the readme file for install instructions.
      coqserapi
      coqserapi
      JavaScript
      •
      GNU Lesser General Public License v2.1
      •6•44•4•29•Updated Mar 23, 2026Mar 23, 2026

    • codemirror-lang-rocq

      Public
      CodeMirror language package for the Rocq proof assistant
      TypeScript
      •
      MIT License
      •0•0•0•0•Updated Mar 3, 2026Mar 3, 2026

    • waterproof-dev

      Public
      Development environment setup for coq-waterproof
      Makefile
      •
      GNU Lesser General Public License v3.0
      •2•0•0•2•Updated Feb 4, 2026Feb 4, 2026

    • introduction-to-proof-sheets

      Public
      Other
      •1•1•1•0•Updated Dec 9, 2025Dec 9, 2025

    • rocq

      Public
      The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and…
      OCaml
      •
      GNU Lesser General Public License v2.1
      •755•0•0•0•Updated Nov 25, 2025Nov 25, 2025

    • waterproof-online

      Public
      An environment to run Waterproof online
      0•0•0•0•Updated Nov 9, 2025Nov 9, 2025

    • waterproof-dependencies-installer

      Public
      Shell
      •2•0•1•0•Updated Nov 4, 2025Nov 4, 2025

    • platform

      Public
      Multi platform setup for Coq, Coq libraries and tools
      Shell
      •
      Creative Commons Zero v1.0 Universal
      •55•0•0•0•Updated Aug 25, 2025Aug 25, 2025

    • waterproof-prairielearn-workspace

      Public
      Dockerfile
      •0•0•0•0•Updated Jul 1, 2025Jul 1, 2025

    • waterproof-alectryon-example

      Public
      Python
      •0•0•0•0•Updated Jun 26, 2025Jun 26, 2025

    • opam-coq-archive

      Public
      Archive for all Coq related OPAM packages organized in various repositories
      OCaml
      •
      GNU Lesser General Public License v2.1
      •135•1•0•0•Updated Aug 27, 2023Aug 27, 2023

    • waterproof-momotor

      Public
      Bridges the gap between waterproof's exercise sheets and momotor's automated grading
      Python
      •
      GNU General Public License v3.0
      •0•0•0•0•Updated Aug 17, 2023Aug 17, 2023

    • coq

      Public
      Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an en…
      OCaml
      •
      GNU Lesser General Public License v2.1
      •755•0•0•0•Updated Jul 31, 2023Jul 31, 2023

    • waterproof-wrapper

      Public
      C++
      •
      GNU Lesser General Public License v2.1
      •0•0•0•0•Updated Nov 14, 2022Nov 14, 2022
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.