mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Server stats:

2.8K
active users

#commonlisp

13 posts12 participants0 posts today
Mistress Remilia<p>Got the NES sound chip emulator working in pure <a href="https://xn--nanako--c83f6n.mooo.com/tags/CommonLisp" rel="nofollow noopener noreferrer" target="_blank">#CommonLisp</a> tonight ​:commonlisp:​<span> The extra chip in the Famicom Disk System is also working.<br><br>Also, as you can see, the port of Benben is coming along nicely. But uhh, ignore the typo I made at first l </span>​:blobcatgiggle:​</p>
Nicolas Martyanoff<p>Having packages/modules be defined as single files is a fundamental programming language design error. <a href="https://fosstodon.org/tags/Python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Python</span></a>, but also <a href="https://fosstodon.org/tags/Erlang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Erlang</span></a>, <a href="https://fosstodon.org/tags/Scheme" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Scheme</span></a>, the misguided package-inferred-system extension for <a href="https://fosstodon.org/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CommonLisp</span></a>… Because no one wants a 10k lines file mixing dozens of concepts, you end up with a multitude of small packages for no good reason. </p><p>At least in Erlang you can just use whatever was loaded without manually importing every single module you need everywhere, but Python is as usual the worst.</p>
Perpetual Beta 🇺🇦<p>Quite happy with myself. Recreated the ubiquitious <a href="https://sonomu.club/tags/supercollider" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>supercollider</span></a> fork function in <a href="https://sonomu.club/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a> with this neat little macro:</p><p>(defmacro fork (&amp;rest func)<br> `(bt:make-thread<br> (lambda ()<br> ,@func<br> (force-output))))</p>
vindarel<p>This gives a very very <a href="https://framapiaf.org/tags/emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>emacs</span></a> -y experience in the browser: <a href="https://lisperator.net/blog/slip-a-lisp-system-in-your-browser/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lisperator.net/blog/slip-a-lis</span><span class="invisible">p-system-in-your-browser/</span></a> </p><p>&gt; This is a <a href="https://framapiaf.org/tags/Lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lisp</span></a> implementation (<a href="https://framapiaf.org/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CommonLisp</span></a> wannabe, but oh well, we're still far from that) that runs in a <a href="https://framapiaf.org/tags/JavaScript" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>JavaScript</span></a> VM. </p><p>Very much inspired by Common Lisp and Emacs/SLIME.</p><p>There's a "crazy clock demo" that runs in a canvas window.</p><p>Impressing.</p>
José A. Alonso<p>Readings shared April 15, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/15-readings_shared_04-15-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/15-readings_shared_04-15-25</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#<span>CommonLisp</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="tag">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="tag">#<span>Lisp</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/RacketLang" class="mention hashtag" rel="tag">#<span>RacketLang</span></a></p>
Mistress Remilia<p><span>tfw your Common Lisp program is using less CPU than your designed-the-same equivalent Crystal program...<br><br>I have my CPU in powersave mode, capped to about 1.9 GHz. It's using 5-10% less CPU decoding and resampling a FLAC file with the sinc-best resampler.<br><br>Either SBCL is just that good of a compiler, SIMD just helps that much, or a bit of both. Probably a bit of both.<br><br></span><a href="https://xn--nanako--c83f6n.mooo.com/tags/CommonLisp" rel="nofollow noopener noreferrer" target="_blank">#CommonLisp</a></p>
screwlisp<p><a href="https://mastodon.sdf.org/tags/LispyGopherClimate" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LispyGopherClimate</span></a> <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> <a href="https://mastodon.sdf.org/tags/ai" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ai</span></a> <a href="https://mastodon.sdf.org/tags/peertube" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>peertube</span></a><br><a href="https://communitymedia.video/w/7KpDL8dmSMN7zH6TxEgQbb" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">communitymedia.video/w/7KpDL8d</span><span class="invisible">mSMN7zH6TxEgQbb</span></a></p><p><span class="h-card"><a href="https://climatejustice.social/@kentpitman" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>kentpitman</span></a></span> <a href="https://mastodon.sdf.org/tags/haiku" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>haiku</span></a> </p><p>Resurrected Sandewall's <a href="https://mastodon.sdf.org/tags/softwareIndividuals" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>softwareIndividuals</span></a> from 2014.</p><p>This episode is dedicated to general purpose interaction in the software individual / <a href="https://mastodon.sdf.org/tags/CAISOR" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CAISOR</span></a> paradigm.</p><p>Next will be porting the dynamicwindows zetalisp zwei to McCLIM <a href="https://mastodon.sdf.org/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a>.</p><p><span class="h-card"><a href="https://merveilles.town/@prahou" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>prahou</span></a></span> <a href="https://mastodon.sdf.org/tags/unix_surrealism" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>unix_surrealism</span></a> next <a href="https://mastodon.sdf.org/tags/openbsd" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>openbsd</span></a> release art??</p><p>Also <span class="h-card"><a href="https://chaos.social/@pesco" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>pesco</span></a></span> and <span class="h-card"><a href="https://mathstodon.xyz/@dougmerritt" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>dougmerritt</span></a></span> on IPE '84</p><p>co guest and join in on <a href="https://mastodon.sdf.org/tags/lambdaMOO" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lambdaMOO</span></a> as always!</p><p><span class="h-card"><a href="https://appdot.net/@mdhughes" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>mdhughes</span></a></span> <span class="h-card"><a href="https://hachyderm.io/@nosrednayduj" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>nosrednayduj</span></a></span> <span class="h-card"><a href="https://social.sachachua.com/@sacha" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>sacha</span></a></span></p>
José A. Alonso<p>The Barium experiment. ~ Tom Szilagyi. <a href="https://tomscii.sig7.se/2025/04/The-Barium-Experiment" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">tomscii.sig7.se/2025/04/The-Ba</span><span class="invisible">rium-Experiment</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#<span>CommonLisp</span></a></p>
Perpetual Beta 🇺🇦<p>Periodic reminder that <a href="https://sonomu.club/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a> is awesome! Delving more and more into the loop construct. It's amazing what is possible to do with it...</p>
screwlisp<p><span class="h-card"><a href="https://mastodon.social/@pedromj" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>pedromj</span></a></span> seeing your iterative and recursive ones helped me see what I was /meant/ to do with series (which should be lazy and declarative):<br>``` <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonLisp</span></a> <a href="https://mastodon.sdf.org/tags/series" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>series</span></a> <br>(defun better-fibs<br> (n &amp;optional (x-1 0) (x-0 1))<br> (let* ((range (scan-range))<br> (fibonacci-series<br> (<a href="https://mastodon.sdf.org/tags/M" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>M</span></a>(lambda (n)<br> (declare (ignore n))<br> (psetq x-1 x-0<br> x-0 (+ x-1 x-0))<br> (values x-0))<br> range)))<br> (collect-nth n fibonacci-series)))<br>```<br>CL-USER&gt; (better-fibs 4)<br>8</p><p>(Edit: (scan-range) on its own is just 𝗡)</p>
lispm<p><span class="h-card" translate="no"><a href="https://fosstodon.org/@amoroso" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>amoroso</span></a></span> <a href="https://mastodon.social/tags/clos" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>clos</span></a> <a href="https://mastodon.social/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a> <a href="https://mastodon.social/tags/oop" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>oop</span></a> <a href="https://mastodon.social/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> there was still a choice between various proposals then...</p><p>But the actual CLOS was not far away - the standard proposal was published in September 1988: <a href="https://dl.acm.org/toc/sigplan/1988/23/SI" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">dl.acm.org/toc/sigplan/1988/23</span><span class="invisible">/SI</span></a> <br>Available above as a PDF. The final version was then published with the ANSI CL standard.</p>
Paolo Amoroso<p>As installments of the ARTIFICIAL INTELLIGENCE column by Ernest Tello, in 1987 Dr. Dobb's Journal published a series of articles on OOP and object-oriented extensions for Common Lisp and Scheme. Back then CLOS was not yet on the radar but the Common Lisp extensions the articles covered already contained the main ideas of CLOS.</p><p><a href="https://archive.org/details/1987-03-dr-dobbs-journal/page/126/mode/2up?view=theater" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">archive.org/details/1987-03-dr</span><span class="invisible">-dobbs-journal/page/126/mode/2up?view=theater</span></a></p><p><a href="https://archive.org/details/1987-04-dr-dobbs-journal/page/146/mode/2up?view=theater" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">archive.org/details/1987-04-dr</span><span class="invisible">-dobbs-journal/page/146/mode/2up?view=theater</span></a></p><p><a href="https://archive.org/details/1987-05-dr-dobbs-journal/page/132/mode/2up?view=theater" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">archive.org/details/1987-05-dr</span><span class="invisible">-dobbs-journal/page/132/mode/2up?view=theater</span></a></p><p><a href="https://fosstodon.org/tags/oop" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>oop</span></a> <a href="https://fosstodon.org/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CommonLisp</span></a> <a href="https://fosstodon.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> <a href="https://fosstodon.org/tags/retrocomputing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>retrocomputing</span></a></p>
screwlisp<p><a href="https://codeberg.org/tfw/pawn-75#headline-13" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">codeberg.org/tfw/pawn-75#headl</span><span class="invisible">ine-13</span></a><br><a href="https://mastodon.sdf.org/tags/Sandewall" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Sandewall</span></a> <a href="https://mastodon.sdf.org/tags/SoftwareIndividuals" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SoftwareIndividuals</span></a> </p><p>creating a knowledgebase, setting it as active, creating a file and</p><p>Minimally defining<br>- an entity that provides a <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> function in the host <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonLisp</span></a> <br>- an entity that provides a new CLE verb in the host <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonLisp</span></a> </p><p>baby steps</p>
screwlisp<p>I realized that I should have two <a href="https://mastodon.sdf.org/tags/slime" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>slime</span></a> repls open, one running a Sandewallian software individual clisp-repl and one McCLIM running ecl-repl (or what have you) and things are getting weird.</p><p>This is because the software individual with a beliefbase about using McCLIM is /not/ the McCLIM lisp image itself, it is a separate lisp image that contains beliefs and actions for using McCLIM in another image. Which is trivial in <a href="https://mastodon.sdf.org/tags/emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>emacs</span></a> with slime. <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonLisp</span></a> <a href="https://mastodon.sdf.org/tags/notThatCommonThoughTeeBeeAitch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>notThatCommonThoughTeeBeeAitch</span></a></p>
Perpetual Beta 🇺🇦<p>Made myself a tiny little package to control the best <a href="https://sonomu.club/tags/daw" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>daw</span></a> in the world <a href="https://sonomu.club/tags/reaper" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>reaper</span></a> with the finest programming language available <a href="https://sonomu.club/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a> :-D</p><p><a href="https://codeberg.org/kflak/cl-reaper" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">codeberg.org/kflak/cl-reaper</span><span class="invisible"></span></a></p>
Konrad Hinsen<p><span class="h-card" translate="no"><a href="https://social.jlamothe.net/profile/me" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>me</span></a></span> I believe that I live in the Real World, though I cannot prove it. And I use <a href="https://scholar.social/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CommonLisp</span></a>, for personal projects and for computational science.</p>
vindarel<p><span class="h-card" translate="no"><a href="https://social.jlamothe.net/profile/me" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>me</span></a></span> You can find here 2 interviews of small teams using CL. One "secretly", one in a great open-source product:</p><p>"questions to Alex Nygren of Kina Knowledge, using Common Lisp extensively in their document processing stack"<br><a href="https://lisp-journey.gitlab.io/blog/lisp-interview-kina/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lisp-journey.gitlab.io/blog/li</span><span class="invisible">sp-interview-kina/</span></a></p><p>"Arnold Noronha of Screenshotbot: from Facebook and Java to Common Lisp."<br><a href="https://lisp-journey.gitlab.io/blog/lisp-interview-screenshotbot/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lisp-journey.gitlab.io/blog/li</span><span class="invisible">sp-interview-screenshotbot/</span></a></p><p><a href="https://framapiaf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> <a href="https://framapiaf.org/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a></p>
vindarel<p><span class="h-card" translate="no"><a href="https://social.jlamothe.net/profile/me" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>me</span></a></span> Personally, as a solo developer, I use CL more and more in my stack, ditching Python the more I can. I wrote about it: <a href="https://lisp-journey.gitlab.io/blog/running-my-4th-lisp-script-in-production/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lisp-journey.gitlab.io/blog/ru</span><span class="invisible">nning-my-4th-lisp-script-in-production/</span></a></p><p>Instead of extending a Python software I&nbsp;write independent modules in CL. It works well for standalone scripts too (read a DB, process data, send everything to a FTP, to a web service, by email…) It's such a joy.</p><p>On Discord, we see some are in big tech©, wrote their personal tool in CL and now it's part of the team's stack.</p><p><a href="https://framapiaf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> <a href="https://framapiaf.org/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonlisp</span></a></p>
andros<p>Me encanta programar en <a href="https://activity.andros.dev/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lisp</span></a> en mi tiempo libre. La programación funcional fomenta la abstracción y me permite construir sistemas complejos a partir de funciones simples. El REPL me abre la puerta a jugar en tiempo real con el código sin tener que reiniciar constantemente el software o forzarme a lanzar un programa de depuración. Para mi es una herramienta poderosa para afinar mis habilidades de programador, probar nuevas ideas, patrones y un espacio para la creatividad. Además tienes sabores en cualquier lugar: <a href="https://activity.andros.dev/tags/clojure" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Clojure</span></a> para JVM, <a href="https://activity.andros.dev/tags/clojurescript" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClojureScript</span></a> para <a href="https://activity.andros.dev/tags/javascript" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>JavaScript</span></a>, <a href="https://activity.andros.dev/tags/emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Emacs</span></a> Lisp para Emacs, <a href="https://activity.andros.dev/tags/commonlisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CommonLisp</span></a> y <a href="https://activity.andros.dev/tags/racket" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Racket</span></a> para ejecutar en el equipo... Aunque yo te recomiendo que te quedes en un solo lenguaje y lo domines. No es necesario aprender todos los dialectos de Lisp, pero si es bueno conocerlos para entender sus diferencias y similitudes.<br>Si quieres aprender más sobre <a href="https://activity.andros.dev/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lisp</span></a>, te recomiendo uno de mis libros favoritos: "Land of Lisp" de Conrad Barski. Es un libro divertido que te enseña a programar en Lisp mientras creas juegos y aplicaciones gráficas. También puedes encontrar muchos recursos en línea, por supuesto.<br></p>
José A. Alonso<p>Readings shared April 10, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/10-readings_shared_04-10-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/10-readings_shared_04-10-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="tag">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#<span>CommonLisp</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="tag">#<span>Reasoning</span></a></p>