Docs About
About Room to Prove
Room to Prove 0.1.0
A free desktop app for reading, writing and exploring mathematics and computer science.
When a newer version is out, the app says so in a small card. It installs it when you press Update and relaunch, and never by itself.
Help → Check for Updates… asks now. Downloads: roomtoprove.com.
Feedback
Tell us what works, what doesn't, and what you'd like.
- In the app: Help → Send Feedback…, or Send feedback in the sidebar.
- By email: developer@gghomology.com.au.
The app shows everything it adds to your message: its version and your system. Your own mail sends it.
Your privacy
No account. No tracking. Your drafts, figures and settings stay on your computer.
Once a day, while it is open, the app asks our download server for one small file: is there a newer version? Nothing about you or your work is sent.
Everything else goes online only when you ask:
| When you… | It contacts |
|---|---|
| set up Lean | Lean's and Mathlib's servers |
| look up a reference | public catalogues, with your search words |
| ask the assistant | the model service you chose (a local model sends nothing) |
| install a plugin | where that plugin comes from |
| update the app | our download server, for the new version |
| send feedback | nothing: your own mail sends it |
Free space, or uninstall
Help → Free Space or Uninstall… shows what the app keeps, with sizes.
- Remove Lean and Mathlib to free about 11 GB. Set them up again at any time.
- Uninstall Room to Prove… removes everything the app downloaded, its settings and saved keys, and moves the app to the Trash.
- Your drafts are moved to a folder in Documents first, unless you choose to delete them.
Thanks
Room to Prove is built on the work of many people.
| Project | Does | Licence |
|---|---|---|
| Lean 4 | checks every proof; brings nanoda, the second checker | Apache-2.0 |
| Mathlib | the library of mathematics | Apache-2.0 |
| MathJax | typesets every formula | Apache-2.0 |
| Tauri | the app's window and core | MIT or Apache-2.0 |
| React | the page | MIT |
| CodeMirror | the editors | MIT |
| Pyodide | Python in the app | MPL-2.0 |
| NumPy, SciPy, SymPy | computation in Python | BSD-3-Clause |
| Matplotlib | plots | Matplotlib licence |
| goose | the assistant's engine | Apache-2.0 |
| CSLib | computer science in Lean | Apache-2.0 |
| LeanTeX, by Kyle Miller | the design of the TeX printer | Apache-2.0 |
The way proofs are shown owes much to Lean's infoview, Paperproof, Verbose Lean, Informal Lean, Verso and Alectryon.
References come from Crossref, arXiv, dblp, OpenAlex and Wikidata (CC0), and Mathlib's bibliography (Apache-2.0).
Every package the app is built from:
The page, from npm: 138 packages.
| Licence | Packages | |
|---|---|---|
| MIT | 123 | @codemirror/autocomplete, @codemirror/commands, @codemirror/lang-css, @codemirror/lang-html, @codemirror/lang-javascript, @codemirror/lang-markdown, @codemirror/lang-python, @codemirror/language, @codemirror/legacy-modes, @codemirror/lint, @codemirror/search, @codemirror/state, @codemirror/streamparser, @codemirror/view, @lezer/common, @lezer/css, @lezer/highlight, @lezer/html, @lezer/javascript, @lezer/lr, @lezer/markdown, @lezer/python, @marijn/find-cluster-break, @types/debug, @types/hast, @types/katex, @types/mdast, @types/ms, @types/unist, @xmldom/xmldom, bail, balanced-match, brace-expansion, ccount, character-entities, character-entities-html4, character-entities-legacy, character-reference-invalid, codemirror, commander, crelt, debug, decode-named-character-reference, dequal, devlop, escape-string-regexp, extend, is-alphabetical, is-alphanumerical, is-decimal, is-hexadecimal, is-plain-obj, katex, longest-streak, markdown-table, mdast-util-directive, mdast-util-find-and-replace, mdast-util-from-markdown, mdast-util-gfm, mdast-util-gfm-autolink-literal, mdast-util-gfm-footnote, mdast-util-gfm-strikethrough, mdast-util-gfm-table, mdast-util-gfm-task-list-item, mdast-util-math, mdast-util-phrasing, mdast-util-to-markdown, mdast-util-to-string, micromark, micromark-core-commonmark, micromark-extension-directive, micromark-extension-gfm, micromark-extension-gfm-autolink-literal, micromark-extension-gfm-footnote, micromark-extension-gfm-strikethrough, micromark-extension-gfm-table, micromark-extension-gfm-tagfilter, micromark-extension-gfm-task-list-item, micromark-extension-math, micromark-factory-destination, micromark-factory-label, micromark-factory-space, micromark-factory-title, micromark-factory-whitespace, micromark-util-character, micromark-util-chunked, micromark-util-classify-character, micromark-util-combine-extensions, micromark-util-decode-numeric-character-reference, micromark-util-decode-string, micromark-util-edit-map, micromark-util-encode, micromark-util-html-tag-name, micromark-util-normalize-identifier, micromark-util-resolve-all, micromark-util-sanitize-uri, micromark-util-subtokenize, micromark-util-symbol, micromark-util-types, ms, parse-entities, react, react-dom, remark-directive, remark-gfm, remark-math, remark-parse, remark-stringify, scheduler, stringify-entities, style-mod, trough, unified, unist-util-is, unist-util-remove-position, unist-util-stringify-position, unist-util-visit, unist-util-visit-parents, vfile, vfile-message, w3c-keyname, wicked-good-xpath, zwitch |
| BlueOak-1.0.0 | 7 | glob, lru-cache, minimatch, minipass, package-json-from-dist, path-scurry, rimraf |
| Apache-2.0 | 5 | @mathjax/mathjax-newcm-font, @mathjax/src, mhchemparser, mj-context-menu, speech-rule-engine |
| MIT OR Apache-2.0 | 2 | @tauri-apps/plugin-process, @tauri-apps/plugin-updater |
| Apache-2.0 OR MIT | 1 | @tauri-apps/api |
The core, from crates.io: 471 crates.
| Licence | Packages | |
|---|---|---|
| MIT OR Apache-2.0 | 222 | aes, android_system_properties, anyhow, arbitrary, async-broadcast, async-recursion, async-trait, base64, bitflags, block-buffer, block-padding, bumpalo, camino, cargo-platform, cbc, cfg-if, chrono, cipher, cookie, core-foundation, core-foundation-sys, core-graphics, core-graphics-types, cpufeatures, crc32fast, crossbeam-channel, crossbeam-utils, crypto-common, dbus-secret-service, deranged, derive_arbitrary, digest, dirs, dirs-sys, displaydoc, dtoa, dyn-clone, embed_plist, enumflags2, enumflags2_derive, erased-serde, errno, fdeflate, field-offset, filetime, flate2, foreign-types, foreign-types-macros, foreign-types-shared, form_urlencoded, futures-channel, futures-core, futures-executor, futures-io, futures-macro, futures-sink, futures-task, futures-util, getrandom, glob, hashbrown, heck, hermit-abi, hex, hkdf, hmac, html5ever, http, httparse, httpdate, iana-time-zone, iana-time-zone-haiku, ident_case, idna, inout, ipnet, itoa, jni, jni-macros, jni-sys, jni-sys-macros, js-sys, json-patch, jsonptr, keyboard-types, keyring, libc, lock_api, log, markup5ever, mime, ndk, ndk-context, ndk-sys, num, num-bigint, num-complex, num-conv, num-integer, num-iter, num-rational, num-traits, once_cell, openssl-probe, ordered-stream, osakit, parking_lot, parking_lot_core, percent-encoding, piper, png, powerfmt, ppv-lite86, proc-macro-crate, proc-macro-error, proc-macro-error-attr, proc-macro2, quote, rand, rand_chacha, rand_core, ref-cast, ref-cast-impl, regex, regex-automata, regex-syntax, reqwest, rustls-pki-types, rustls-platform-verifier, rustls-platform-verifier-android, rustversion, scopeguard, secret-service, security-framework, security-framework-sys, semver, serde, serde-untagged, serde_core, serde_derive, serde_derive_internals, serde_json, serde_path_to_error, serde_repr, serde_spanned, serde_with, serde_with_macros, serialize-to-javascript, serialize-to-javascript-impl, servo_arc, sha1, sha2, signal-hook-registry, simdutf8, siphasher, smallvec, socket2, softbuffer, stable_deref_trait, static_assertions, string_cache, swift-rs, syn, system-configuration, system-configuration-sys, tao-macros, tar, tempfile, tendril, thiserror, thiserror-impl, time, time-core, time-macros, tokio-rustls, toml, toml_datetime, toml_edit, toml_parser, toml_writer, tray-icon, typed-path, typeid, typenum, unicode-segmentation, url, wasm-bindgen, wasm-bindgen-futures, wasm-bindgen-macro, wasm-bindgen-macro-support, wasm-bindgen-shared, wasm-streams, web-sys, web-time, web_atoms, winapi, winapi-i686-pc-windows-gnu, winapi-x86_64-pc-windows-gnu, windows, windows-collections, windows-core, windows-future, windows-implement, windows-interface, windows-link, windows-numerics, windows-registry, windows-result, windows-strings, windows-sys, windows-targets, windows-threading, windows-version, windows_aarch64_gnullvm, windows_aarch64_msvc, windows_i686_gnu, windows_i686_gnullvm, windows_i686_msvc, windows_x86_64_gnu, windows_x86_64_gnullvm, windows_x86_64_msvc, xattr |
| MIT | 113 | atk, atk-sys, axum, axum-core, block2, bytes, cairo-rs, cairo-sys-rs, cargo_metadata, cfb, combine, darling, darling_core, darling_macro, derive_more, derive_more-impl, dlopen2, dlopen2_derive, dom_query, endi, gdk, gdk-pixbuf, gdk-pixbuf-sys, gdk-sys, gdkwayland-sys, gdkx11, gdkx11-sys, generic-array, gio, gio-sys, glib, glib-macros, glib-sys, gobject-sys, gtk, gtk-sys, gtk3-macros, http-body, http-body-util, hyper, hyper-util, ico, infer, is-docker, is-wsl, javascriptcore-rs, javascriptcore-rs-sys, libredox, memoffset, minisign-verify, mio, new_debug_unreachable, nix, objc2, objc2-encode, objc2-foundation, open, pango, pango-sys, phf, phf_generator, phf_macros, phf_shared, plist, precomputed-hash, quick-xml, redox_syscall, redox_users, rfd, schannel, schemars, schemars_derive, simd-adler32, slab, soup3, soup3-sys, strsim, synstructure, tokio, tokio-macros, tokio-util, tower, tower-http, tower-layer, tower-service, tracing, tracing-attributes, tracing-core, trash, try-lock, uds_windows, urlencoding, urlpattern, want, webkit2gtk, webkit2gtk-sys, webview2-com, webview2-com-macros, webview2-com-sys, which, winnow, x11, x11-dl, xdg-home, zbus, zbus_macros, zbus_names, zcheapstr, zip, zmij, zvariant, zvariant_derive, zvariant_utils |
| Apache-2.0 OR MIT | 50 | async-channel, async-executor, async-fs, async-io, async-lock, async-process, async-signal, async-task, atomic-waker, bit-set, bit-vec, blocking, cesu8, concurrent-queue, ctor, dbus, equivalent, event-listener, event-listener-strategy, fastrand, futures-lite, idna_adapter, indexmap, libappindicator, libappindicator-sys, libdbus-sys, muda, parking, pin-project-lite, polling, rustc-hash, simd_cesu8, tauri, tauri-codegen, tauri-macros, tauri-plugin-dialog, tauri-plugin-fs, tauri-plugin-opener, tauri-plugin-process, tauri-plugin-updater, tauri-runtime, tauri-runtime-wry, tauri-utils, utf8_iter, utf_types, uuid, window-vibrancy, wry, zeroize, zeroize_derive |
| Unicode-3.0 | 18 | icu_collections, icu_locale_core, icu_normalizer, icu_normalizer_data, icu_properties, icu_properties_data, icu_provider, litemap, potential_utf, tinystr, writeable, yoke, yoke-derive, zerofrom, zerofrom-derive, zerotrie, zerovec, zerovec-derive |
| Zlib OR Apache-2.0 OR MIT | 17 | bytemuck, dispatch2, objc2-app-kit, objc2-cloud-kit, objc2-core-data, objc2-core-foundation, objc2-core-graphics, objc2-core-image, objc2-core-location, objc2-core-text, objc2-exception-helper, objc2-io-surface, objc2-osa-kit, objc2-quartz-core, objc2-ui-kit, objc2-user-notifications, objc2-web-kit |
| Unlicense OR MIT | 6 | aho-corasick, byteorder, memchr, same-file, walkdir, winapi-util |
| BSD-3-Clause | 6 | alloc-no-stdlib, alloc-stdlib, subtle, zstd, zstd-safe, zstd-sys |
| MPL-2.0 | 5 | cssparser, cssparser-macros, dtoa-short, option-ext, selectors |
| Apache-2.0 WITH LLVM-exception OR Apache-2.0 OR MIT | 5 | linux-raw-sys, rustix, wasi, wasip2, wit-bindgen |
| Apache-2.0 OR ISC OR MIT | 3 | hyper-rustls, rustls, rustls-native-certs |
| ISC | 3 | libloading, rustls-webpki, untrusted |
| Apache-2.0 | 3 | sync_wrapper, tao, zopfli |
| CC0-1.0 OR MIT-0 OR Apache-2.0 | 2 | constant_time_eq, dunce |
| Zlib | 2 | foldhash, zlib-rs |
| BSD-3-Clause OR MIT OR Apache-2.0 | 2 | num_enum, num_enum_derive |
| BSD-2-Clause OR Apache-2.0 OR MIT | 2 | zerocopy, zerocopy-derive |
| 0BSD OR MIT OR Apache-2.0 | 1 | adler2 |
| BSD-3-Clause AND MIT | 1 | brotli |
| BSD-3-Clause OR MIT | 1 | brotli-decompressor |
| Apache-2.0 AND MIT | 1 | dpi |
| Apache-2.0 OR MIT | 1 | fnv |
| MIT AND BSD-3-Clause | 1 | matchit |
| MIT OR Zlib OR Apache-2.0 | 1 | miniz_oxide |
| MIT OR Apache-2.0 OR LGPL-2.1-or-later | 1 | r-efi |
| MIT OR Apache-2.0 OR Zlib | 1 | raw-window-handle |
| Apache-2.0 AND ISC | 1 | ring |
| (MIT OR Apache-2.0) AND Unicode-3.0 | 1 | unicode-ident |
| CDLA-Permissive-2.0 | 1 | webpki-root-certs |
Licence
Room to Prove is licensed under the Apache License, Version 2.0. Use it freely, for any purpose. It comes as is, without warranty.