Life & fun · February 10, 2025
Lapisla – A Theorem Proving Platform for Openness and Reusability
Hey HN! We built *lapisla*, a theorem proving platform designed to make formal proofs more open and collaborative. We developed a kernel, editor, proof registry, and platform ── all accessible directly in the browser. Why we built this: Existing theorem provers are powerful, but they often feel isolated and difficult to extend. Unlike modern programming languages, which thrive on package managers and shared libraries, theorem proving tools lack a seamless way to integrate others' work. lapisla aims to bridge this gap by: * Offering a verified public proof registry for sharing and discovering…
What it does
In the maker’s words, at launch
Hey HN! We built *lapisla*, a theorem proving platform designed to make formal proofs more open and collaborative. We developed a kernel, editor, proof registry, and platform ── all accessible directly in the browser. Why we built this: Existing theorem provers are powerful, but they often feel isolated and difficult to extend. Unlike modern programming languages, which thrive on package managers and shared libraries, theorem proving tools lack a seamless way to integrate others' work. lapisla aims to bridge this gap by: * Offering a verified public proof registry for sharing and discovering proofs (all proofs are checked upon registration) * Being fully browser-based. No installation needed * Supporting permanent links to easily share proofs Future Plans: Currently, lapisla runs on our own kernel, but we envision supporting multiple kernels in the future. We want lapisla to be a general platform for formal reasoning, where users can choose and experiment with different proof engines. Of course, we love our kernel, so we'll continue to make it as powerful as possible. We are also planning a search registry like Hoogle, automated theorem proving, and more. Try it out! Reference: * https://lapisla.net/ – Explore and write your proof ! * https://docs.lapisla.net/ – Documentation * https://trap.jp/post/2478/ – We built this as a team of university friends during a one-week hackathon (plus two weeks of minor refinements). This is our blog post about the development. (Sorry, it's in Japanese.) We’d love your feedback!
Does the same job
all alternatives →- DTDependently typed language for proofs that you can implement in one day2021 · github.com · ▲138
- ISI started a repo for sharing algorithm implementations2013 · github.com · ▲52
Everything that would be here is in the README. I hope this gets big, it has tons of potential.
- CFClojure for the Brave and True – now free online2015 · braveclojure.com · ▲224
- EAEole, a Lévy-optimal lambda calculus evaluator written in Rust2019 · github.com · ▲106
- ZKZero-Knowledge Proofs in WebAssembly2019 · zkwasm.kobi.one · ▲81
- PCProof Companion – Geometry proof practice for students2017 · proofcompanion.com · ▲64
More life & fun this month
the category →- TL
Life & fun · 10d ago · louisabraham.github.io
Photosynthesis fires two of your iPhone
Life & fun · 28d ago · photosynthesis.camera
SoloUno▲310Take control of hair pulling, nail biting & skin picking
Life & fun · 28d ago · solouno.io
Scroll through all 43,252,003,274,489,856,000 reachable Rubik's Cube permutations.
Life & fun · 26d ago · everycube.alen.is
Hi HN, I built Eigendrum, a web tool that solves the 2D wave equation for arbitrary shapes so you can hear what they sound like as drums. How it works: * Solves -∇²u = λu using finite element analysis (Kφ = λMφ) on a triangle mesh. * Validated to <0.1% error against closed-form solutions for circles (Bessel zeros) and rectangles. * Sound model factors in strike location, Rayleigh damping, and mallet width. * Includes Kac drums I & II to demonstrate identical sound spectra from different geometries. * No frameworks, build steps, or dependencies. Repo and tests:…
Life & fun · 26d ago · baselashraf81.github.io
Launched alongside, February 2025
the whole month →
Screen Studio 3.0▲1,833Beautiful screen recordings with instant shareable links
Growth · 2025 · screen.studio
- IG
I was at FB/Meta from late 2013 to early 2023, mostly working in the compiler/runtime spaces. I got hit in the spring 2023 layoff wave. I immediately started making games in my newfound free time (a lifelong interest, and I even worked in AA(A?) back ca. ~2000), and in October 2023 I stumbled upon the idea of a roguelike pachinko/plinko game inspired by Luck Be A Landlord. Things snowballed quickly, I started talking to publishers, then worked like crazy through all of 2024, almost the hardest I've ever worked in my career, and launched the game in December 2024. It's sold…
Work · 2025
- IB
i wanted to change the habit of reaching for my phone in the morning and doomscrolling away an hour so i built an app to help me. now i have to literally touch grass before accessing my most distracting apps the app is built in swiftui, uses the screen time apis provided by apple and google vision to recognise grass or not i'd love to get your thoughts on the concept.
Life & fun · 2025 · touchgrass.now