Your periodic reminder that trying to pull the speedometer needle over to the right will not make your vehicle go any faster.
#ProxyMetrics #Lean #Safe #DORA

J'ai découvert le mot et le concept d'#Obeya

https://notes.sklein.xyz/2025-07-01_1225/

Rappel , j'organise un meetup sur le #darkLean le #lean qui respecte pas les gens !
C'est mardi prochain, c'est à @OCTOTechnology et il y aura des intervenants de @theodo !
Plus d'info ici => https://www.linkedin.com/feed/update/urn:li:activity:7330610356643319810/
#Agile #extremeAgilité

TIL that MPV is the best sh player for Android I've seen. I have been looking for a player which gives me the output like mPlayer Linux for decades!

Thanks to @rl_dane & @joel who talked about music players on Android

On a more positive note re screwing around with #Lean:

I don't like the principle of explosion, but I think I now understand a little better why some mathematicians insist on it. Specifically, suppose you have (a ∨ b) b. If a is false, this statement becomes tautological. The folks behind Lean have chosen to put this in as a rewrite rule:
((a ∨ b) b) ⇒ (a →b) and then you prove ¬a and you apply the principle of explosion.

screwing around with #Lean has mainly served to confirm my prior suspicion that LSPs need to be a lot lighter weight before I'll be interested in using them on a day-to-day basis. I do not appreciate it when my editor lags and my computer's fans howl because some kind of compilation process is being repeated for every keystroke *while I'm in the middle of writing a comment*.

On refait un meetup #eXtremeAgilité sur le coté sombre du #lean chez #OCTOTechnology le 27 mai avec Julien Calixte et Guillaume Gremillet de #theodo !
Venez nombreux !

https://forms.gle/mb2GBGM6DDMSbYwz5

I recently set myself the exercise of using modern automated tools - in particular, a combination of the #GithubCopilot large language model and the dependent type matching tactic #canonical - to try to semi-automatically formalize in #Lean a one-page proof provided by a collaborator of the #EquationalTheoriesProject (Bruno Le Floch). With these tools, I was able to more or less blindly do the formalization in 33 minutes, withou any real high level conception of how the proof proceeded. It was a very different style to how I usually formalize results, but was workable for this type of technical, non-conceptual argument where the main issue is to get the details correct rather than the "big picture".

I recorded my attempt at https://www.youtube.com/watch?v=cyyR7j2ChCI . See also additional discussion at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2 . The final proof (which is far from optimized, but got the job done) can be found at https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean

Suspense insoutenable !

Rendez-vous les 1er et 2 avril 2025 à Paris (Beffroi de Montrouge)

Programme complet de la conférence : https://lnkd.in/eRmf8Rki

Toutes les infos sont disponibles sur le site : https://lnkd.in/e6Xh8evJ

#agile #lean #toc #intelligencecollective
@numerique_gouv

As part of our (@sarantja@mastodon.social and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.

We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.

Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS

You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).

P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.

Less Is More: A Guide to Cleaner Composition | Fstoppers https://fstoppers.com/education/less-more-guide-cleaner-composition-692408?utm_source=flipboard&utm_content=topic/photography
#photography #composition #lean

The "Lean for Mathematicians" workshop, aimed at training graduate students and postdocs in the use of the #Lean proof assistant language for mathematics, runs June 16-27 2025 and is currently taking applications. https://sites.google.com/view/simonsleanworkshop2025

Un premier livre #lean, fruit d'une communauté de pratique... Avec un morceau de ma prose dedans ! Et surtout celle des autres membres de l'@ilf

https://onpk.net/index.php/2025/01/21/900-un-premier-livre-fruit-d-une-communaute

@Godefroy_B Je suis en train de préparer une liste de praticiens #Lean sur Mastodon : https://fedidevs.com/s/MzA0/

Et malheureusement je ne pas ajouter le compte de @ilf parce qu'il n'est pas "découvrable". Si tu as envie que je l'ajoute dans la liste, il suffit que tu coches la case "Autoriser des algorithmes de découverte à mettre en avant votre profil et vos messages" dans le profil ;-) Possible ?

Dernier échange en date : toujours du #lean, cette fois sous la forme d’un "rubber duck gemba walk"

https://noparking.net/post-quand-un-canard-en-plastique-regarde-le-gemba