← Feed

Posts

• Post #2798895

  @kha opening the first #leanprover meetup in Munich

• Post #2798894

  @ejgallego blew my mind with a demo where he had an imperative language embedded in Lean (always nice, of course, but nothing new so far), and then vibe-coded a debugger for it, with a graphical UI and DAP support, on top of it. This really makes #Leanprover shine. More details at https://www.joachim-breitner.de/blog/819-Vibe-coding_a_debugger_for_a_DSL

• Post #2798893

  Formalizing research #mathematics with #leanprover is normal these days, but now people are formalizing #physics results as well, to bring it up to that level of rigor – and already the first paper they look at falls apart, with the main theorem being (provably) incorrect: https://arxiv.org/abs/2603.08139

• Post #2798892

  I participated into a study on how I use Lean They anonymized the transcript for some research repository, and asked me to approve that. I pasted that transscript into Gemini, and immediately got: SPEAKER_01 is an advanced user and developer of the Lean theorem prover. While the transcript doesn't explicitly state a name, the speaker provides very specific biographical and technical details that strongly suggest they are Joachim Breitner. Key Identifying Details: […] Anonymization i...

• Post #2798891

  RE: https://mastodon.social/@fm_volker/116205304864670485 AI can be brutally honest: about how little human intelligence some of our daily tasks actually need, about how incomplete human peer review is, and how fig-leafy some anonymization attempts are. Maybe that’s a good thing.

• Post #2798890

  RE: https://discuss.systems/@bobkonf/116221261428106677 I showed up this morning at breakfast at #bobkonf looking forward to some relaxed listening to tasks, when the organizer approached me and asked if can spontaneously fill a slot. So I did and gave a #leanProver talk. This keeps happening to me, that's how I ended up giving a talk here last year 🤷🏻

• Post #2798889

  Chris Smith writes a nice blog post touching on probability theory and psychology: https://cdsmithus.medium.com/to-flip-or-not-to-flip-d4811e66120b

• Post #2798888

  Very nicely done video by @david explaining some of my work on #leanprover and well-founded recursion: https://youtu.be/LOUbbiV0mWc

• Post #2798887

• Post #2798886

  Why is there no Isar-like structured proof mode in Lean, like there is for Isabelle? In https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Thoughts.20about.20Isar.20and.20Lean/near/591162685 I offer two answers: 1. There is now (AI-assistet proof of concept): https://github.com/nomeata/lean-lisar, proving that it's certainly well possible. 2. It doesn’t seem to be needed that much. (Assume it were. Someone would have built it if it is possible. And from the point above...