Meven Lennon-Bertrand
mevenlennonbertrand@lipn.info
<p>Post-doc at INRIA/IRIF/Université Paris Cité.</p><p>I mostly try to convince proof assistants that they are doing reasonable things. Sometimes this involves studying type theory. Sometimes this means understanding what our implementations do. All in all, it's not too bad.</p><p>Profile banner (from the Leonard comic by Turk & de Groot):<br />- I wanted to serve science because it it my joy and instead of that, what am I doing?...<br />- Yes, what is he doing?<br />- I guess he's complaining!</p>
Posts
-
Post #4165797
This whole Lean kernel bug is almost too on point to be true, it fits perfectly in the discussions we've had here and elsewhere over the last months/years… To summarize: - an AI agent let loose provides a sorry-free proof of the Collatz conjecture - the proof is detected as actually being a kernel bug - the bug is related to (nested) inductive types, for which there is no clear theoretical specification: the kernel's code is the reference - external checkers (lean4lean and nanoda from a...
-
Post #3453848
@arretsurimages@mamot.fr trahi par ses liens... Pour un média qui analyse la déliquescence du paysage informationnel et se rit des faux-pas des autres, c'est assez ironique 😬
-
Post #3288565
@edwinb @gallais I want to cite the fact that Idris 2 has `Type : Type`. Is there anything more authoritative than the note in the FAQ saying “Idris 2 currently implements Type : Type. Don’t worry, this will not be the case forever!”? (Also, just to be sure: is this note still up to date?)
-
Post #2142733
Another day in &quot;having a reliable aka complete kernel is pretty nice&quot;, from @BeLazy: fixing incompleteness issues with η for unit fixes open issues with pattern-matching compilation!? (PR: https://github.com/leanprover/lean4/pull/12636)
-
Post #1629262
Another day, another rant about injectivity: https://proofassistants.stackexchange.com/questions/6533/why-does-lean4-use-intensional-type-theory-when-its-definitional-equality-is-und Am I an old broken record already?
-
Post #1402953
Did you know that Rocq has very good looking badges to include in your next paper/repo/etc? https://github.com/rocq-prover/rocq-prover.org/tree/9529d3ee4f4c86c5cc73650f2c07d06fa458762c/rocq-id/badges
-
Post #674763
Looks like the ACM&#39;s AI summaries are still the only thing appearing whenever you do a search… How do we need to say it!?
-
Post #615304
RE: https://mastoxiv.page/@arXiv_csLO_bot/116169963926058915 Lately I&#39;ve embarked on a fun side quest in proof theory. Where I managed to still bump into bidirectional typing! (To an old dog everything looks like a nail, that&#39;s the saying right?) I learned bidirectionalism is very much related to the subformula property, a proof theory idea that had always seemed mysterious to me. Now I understand why proof theorists rave about cut elimination and the subformula property, which...
-
Post #615300
Did you know: the only image of Michel Rolle available on the internet is, in fact, a low resolution picture of Leibnitz. (Rolle is known by every French math student because the standard construction of analysis here goes through the theorem named after him, is it one of those cases where we&#39;re the only ones doing it this way or is the guy actually famous?)
-
Post #544665
The time has come: Claude is able to poke holes in the dark corners of Rocq&#39;s kernel and come up with proofs of False! The days of &quot;our reasonable users use the unreasonable features only in reasonable ways so it&#39;s ok to have them&quot; really are over. Can&#39;t wait until someone vibe codes a complicated proof without looking too closely at it (since it&#39;s been checked by the kernel, it must be fine!) only to later realise it was actually bogus and such...