{"id":"28e3bb33-491d-47c4-9cc3-34f35237822b","kind":"sos","name":"Careful whispers of proof assistants; Lean4, Nix, Nvim; installation support and demo","slug":"careful-whispers-of-proof-assistants-lean4-nix-nvi","url":"https://api.events.ccc.de/congress/2025/event/28e3bb33-491d-47c4-9cc3-34f35237822b/?format=json","track":null,"assembly":"sos","room":null,"location":"NixOS assembly","language":"en","description":"Lean4 is a proof assistant with an extensive mathematical library. It's also a nice programming language that can be used for formal verification of software. In this impromptu session, I can help get an opinionated Lean4 setup running on your Linux computer using Nix and Neovim. If time permits, I can show how to prove simple theorems, and answer some of the questions that might come up.\r\n\r\nSee https://github.com/kowale/39c3-careful-whispers","schedule_start":"2025-12-29T20:00:00+01:00","schedule_duration":"01:00:00","schedule_end":"2025-12-29T21:00:00+01:00"}