Embed Notice

HTML Code

<blockquote style="position: relative; padding-left: 55px;"><section><a href="https://wandering.shop/users/xgranade/statuses/113676314599658273">Cassandra Granade 🏳️‍⚧️ (xgranade@wandering.shop)'s status on Thursday, 19-Dec-2024 08:01:56 JST</a><a href="https://wandering.shop/@xgranade" title="xgranade@wandering.shop"><img src="https://gnusocial.jp/avatar/114762-48-20230711182559.webp" width="48" height="48" alt="Cassandra Granade 🏳️‍⚧️" style="position: absolute; left: 0; top: 0;">Cassandra Granade 🏳️‍⚧️</a><div><a href="https://mastodon.social/@mcc/113676306788805757" rel="in-reply-to">in reply to</a><ul><li><li><a href="https://gnusocial.jp/user/160011" title="darabos@mastodon.online">Daniel Darabos</a></li></ul></div></section><article><p><a href="https://mastodon.social/@mcc">@mcc</a> <a href="https://mastodon.online/@darabos">@darabos</a> It's a programming language and a theorem solver that checks proofs in that language. I'm not sure if it's technically possible to do AoC challenges in Lean, but I have had a lot of fun learning the language through the Natural Numbers Game (<a href="https://adam.math.hhu.de/#/g/leanprover-community/nng4" rel="nofollow noreferrer">https://adam.math.hhu.de/#/g/leanprover-community/nng4</a>).</p></article><footer><a rel="bookmark" href="https://gnusocial.jp/conversation/4213235#notice-8234381">In conversation</a><time datetime="2024-12-19T08:01:56+09:00" title="Thursday, 19-Dec-2024 08:01:56 JST">about 6 months ago</time> <span>from <span><a href="https://wandering.shop/@xgranade/113676314599658273" rel="external" title="Sent from wandering.shop via ActivityPub">wandering.shop</a></span></span><a href="https://wandering.shop/@xgranade/113676314599658273">permalink</a><h4>Attachments</h4><ol><li><article><header><div>No result found on File_thumbnail lookup.</div><h5><a href="https://adam.math.hhu.de/#/g/leanprover-community/nng4">Lean Game Server</a></h5><div></div></header><div></div><footer></footer></article></li></ol></footer></blockquote>

Corresponding Notice

Embed this notice
Cassandra Granade 🏳️‍⚧️ (xgranade@wandering.shop)'s status on Thursday, 19-Dec-2024 08:01:56 JSTCassandra Granade 🏳️‍⚧️
in reply to
- mcc
- Daniel Darabos
@mcc @darabos It's a programming language and a theorem solver that checks proofs in that language. I'm not sure if it's technically possible to do AoC challenges in Lean, but I have had a lot of fun learning the language through the Natural Numbers Game (https://adam.math.hhu.de/#/g/leanprover-community/nng4).
In conversationabout 6 months ago from wandering.shoppermalink
Attachments
1. No result found on File_thumbnail lookup.
  Lean Game Server

Public

Embed Notice

HTML Code

Corresponding Notice