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!