mastouille.fr est l'un des nombreux serveurs Mastodon indépendants que vous pouvez utiliser pour participer au fédiverse.
Mastouille est une instance Mastodon durable, ouverte, et hébergée en France.

Administré par :

Statistiques du serveur :

673
comptes actifs

#canonical

4 messages4 participants1 message aujourd’hui

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 youtube.com/watch?v=cyyR7j2ChC . See also additional discussion at leanprover.zulipchat.com/#narr . The final proof (which is far from optimized, but got the job done) can be found at github.com/teorth/estimate_too

A répondu dans un fil de discussion

@spaceraser @dan @ossobuffo

Sadly agreed. #LinuxPhones are purely a hobbyist zone right now.

Desktop Linux is 95% there, though.

I'm seriously considering switching my work machine from #Debian to #AuroraLinux, which is immutable #Fedora-based with #KDE #Plasma. I'm still quite happy with Debian, but I want to try something that I can recommend to my coworker who's currently stuck on Windows 10.

The only bummer is that the only distros I can whole-heartedly recommend to beginners are either Fedora or #Ubuntu-based. I cannot wholeheartedly endorse either Fedora as an org (too closely tied to #IBM) or Ubuntu (#Canonical, where is thy soul?).

I dearly love Debian, but a 2-year release cycle is just untenable today. Software changes far too quickly. I had some (minor) things break this year because even the compilers were too old. XD

A répondu dans un fil de discussion

@lga31 @mlo
J'ai essayé pendant un temps #MandrakeLinux puis #Mandriva, mais jamais #Mageia

Je ne nierai pas ma préférence tout de même pour #Ubuntu (pas seulement parce que ça a été ma première distro à 100% et sans dual-boot) ou dérivée.

Certes, elle n'est ni Française ni Européenne, mais d'une part elle a un cycle de vie que je trouve à la fois clair (2 maj majeures/an en avril et octobre) et pertinente (LTS tous les 2 ans) ; et d'autre part #Canonical propose un support professionnel à celui qui le souhaite.