Ayhon @ayhon@qoto.org
Computer Science and Mathematics
Joined Apr 2022
@yosh Any recommendations on where to start?
@lodurel Indeed, I guess I was just questioning the current utility of installing texlive in the first place. Personally the software package has becnisl large that I've chosen to delegate its installation and usage to a third party "in the cloud". Admittedly, I have not yet had to write something as extensive as a PhD thesis, so my situation is different. If I were to do a PhD, I probably would need to have a local installation, and I'd probably not uninstall it until I have to change PCs (and reinstall the OS with it)
@lodurel Honestly, I don't even have Tex installed. If I need to do something that I can't get down with Markdown, I go to Overleaf.
I have videogames installed which take less space than texlive
Ayhon
boosted
I've now published my blog post, "I want a good parallel computer." https://raphlinus.github.io/gpu/2025/03/21/good-parallel-computer.html . Thanks much to all the feedback on the draft, I'd like to think I've clarified some things that might have been confusing.
Ayhon
boosted
There are just a few days left now to register for the Midlands Graduate School (MGS) in Sheffield, 7-11 April 2025. Eight fantastic courses on category theory, type theory, coalgebra, semantics and more.
Registration closes on Monday 24th March.
@MartinEscardo Public tonge?
Ayhon
boosted
The first production ready version of The Rocq Prover 9.0 has been released today, see https://rocq-prover.org/releases/9.0.0 on our new official website! In the coming weeks, we'll migrate the Discourse, Zulip and Github organizations, please bear with us and don't hesitate to report broken links! Packages for opam and nix will be coming soon.
@yosh However, as I understood it, the piece in the system which verifies that the provided "citation" proves the fact the LLM is trying to use is a second LLM. So what protects the system from the second LLM hallucinating?
Probably anything which involves matching strings of text will be fine, but what if it has to do some sort of computation, such as "number of Rs in strawberry"?
Ayhon
boosted
La théorie des types, de Russell aux assistans à la demostration. ~ Thierry Coquand. https://www.youtube.com/live/78CQ2A5_EvI #TypeTheory #ITP #Logic #Math
Ayhon
boosted
Here is a followup to my previous "consolidate #Bevy microblogging" post, which includes our final decision:
https://github.com/bevyengine/bevy/discussions/18302
Ayhon
boosted
that... uh- y- you do realize that... alright then
Ayhon
boosted
was trying to figure out how to implement some algebraic structures based on what i've been learning in my course on automated proof verifiers and anyway that's why i googled "coq rings" your honour
Ayhon
boosted
36th European Summer School in Logic, Language and Information
https://2025.esslli.eu/
Registration is now open for students!
Boosts are appreciated.
Ayhon
boosted
Dear American friends, I know for a fact that many of you were as horrified as I was over the shameless display BLOATUS put on in the Oval Office yesterday.
I decided this morning that rather than seethe about it, I'd do something meaningful with my anger.
Below is the URL of Ukraine's official fundraising page. Maybe you could chip in a small amount, and/or give this a boost to spread the word? Thanks, and remember, there's still many more of us than of them!
Ayhon
boosted
Let's de-Musk social media. Posted in the centre of Berlin.
Thanks to #savesocial @bjoernsta and @hnnng
More at https://savesocial.eu/en/
@yosh I'm on a similar quest this year, and I've been gathering tips from Huberman Lab's podcast. It has helped me a bunch, although I can't say whether it has been placebo or not. I thought I'd share regardless.
https://open.spotify.com/episode/2OZwx69tcePJ1nZfKPQRbu?si=QMSjAj8ETWGH6-4e54GYlA
For now the ones I've been implementing in my schedule are the perception of light in the morning and cold showers.
Ayhon
boosted
Please boost and spread the word.
European alternatives for popular services from the USA. This page is far from perfect or complete but just an illustration that there are alternatives.
https://european-alternatives.eu/alternatives-to
This is also an interesting page with alternatives,
https://www.privacyguides.org/en/tools/
Ayhon
boosted
The second part of Grant Sanderson's video interview with myself on the cosmic distance ladder is now out: https://www.youtube.com/watch?v=hFMaT9oRbs4
I wrote a blog post with additional commentary and corrections on both videos at https://terrytao.wordpress.com/2025/02/13/cosmic-distance-ladder-video-with-grant-sanderson-3blue1brown-commentary-and-corrections/
@kepano Full disclosure, I just realized Graph view is actually already a core plugin. Smh
Computer Science and Mathematics
Joined Apr 2022
