José F. Morales

Beyond Orthogonality: How Language Models Pack Billions of Concepts into 12,000 Dimensions In a recent 3Blue1Brown video series on transformer models, Grant Sanderson posed a fascinating question: How can a relatively modest embedding space of 12,288 dimensions (GPT-3) accommodate millions ...

nickyoder.com/johnson-lind...

These are real images of exoplanets.

Four super-Jupiters, imaged 10 times over 12 years around a star 133 lightyears away.

These are real, giant worlds, out there in the dark.

And we can see them.

George Bernard Shaw: "El secreto de ser desdichado estriba en tener tiempo de pensar si se es, o no, feliz. La cura es la ocupación, porque ocupación significa preocupación; y la persona preocupada no es ni feliz ni infeliz, sino simplemente viva y activa, lo que es más agradable que cualquier ...

75% of US scientists who answered Nature poll consider leaving More than 1,600 readers answered our poll; many said they were looking for jobs in Europe and Canada.

www.nature.com/articles/d41...

Thanks! 😂

I'm Spanish and I do not get it...

What is a quotient? Undergraduate mathematicians usually have a hard time defining functions from quotients in Lean, because they have been taught a specific model for quotients in their classes, which is not the mode…

What is a quotient? ~ Kevin Buzzard. xenaproject.wordpress.com/2025/02/09/w... #ITP #LeanProver #Math

Reddit post: Have we ever considered allowing orphans in bin crates? The main reason for not allowing them is that a dep anywhere in your tree could add a trait and break everything, to put it simply. That's a good reason to disallow them in libs, but for.

Rust community coming strongly in favor of child labor in trash collection

Formally Verified Binary-level Pointer Analysis Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the result is trustworthy...

Formally verified binary-level pointer analysis. ~ Freek Verbeek, Ali Shokri, Daniel Engel, Binoy Ravindran. arxiv.org/abs/2501.17766 #ITP #IsabelleHOL

This is what the government did with 120K+ Japanese Americans in 1942.

I know. I was there in those camps.

C IS LEGAL AGAIN

GitHub - marcusrossel/verified-compiler: A toy example of a verified compiler. A toy example of a verified compiler. Contribute to marcusrossel/verified-compiler development by creating an account on GitHub.

A toy example of a verified compiler. ~ Marcus Rossel. github.com/marcusrossel... #ITP #LeanProver

Ten Years of Blog I noticed as I was reviewing last year that today is the 10 year anniversay of my blog. WOO! 🎉

[New Blog Post] Ten Years of Blog www.philipzucker.com/ten_year_blog/

Teaching "Foundations of mathematics" with the LEAN theorem prover. ~ Mattia Luciano Bottoni, Alberto S. Cattaneo, Elif Sacikara. arxiv.org/abs/2501.03352 #ITP #LeanProver #Math

x.com/debasishg/st...

"A paper from 2008 co-authored by
@yminsky
on why Jane Street started using OCaml for a wide range of tasks: critical trading systems, quantitative research, systems software, and system administration. "
www.cambridge.org/core/journal...

news.ycombinator.com/item?id=4248...

The type theory of Lean: github.com/digama0/lean...

lambdaland.org/posts/2024-1...

elpa.gnu.org/packages/crd... is awesome!

macOS folk: This is your periodic reminder 🎗️ to:

```bash
$ brew update && brew upgrade && brew cleanup
```

I just got back 10.7 GB & patched a slew of CVEs.

Thank you! The repo warns this: "At this time, this will spam others timelines, so it is only recommended to run on new accounts with no followers. See Known problems below for details.". I wonder if I should import my posts now that some people followed me... 😟

LearnSAT: A SAT solver for education. ~ Moti Ben-Ari. github.com/motib/LearnS... #Logic #Prolog #LogicProgramming

GitHub - llaisdy/PrologInfo: Prolog, Datalog, languages, resources, and beyond! Prolog, Datalog, languages, resources, and beyond! - llaisdy/PrologInfo

First draft of a Prolog languages list. Sections on Lambda Prolog, Datalog, and other logic programming languages.
Feedback, PRs, etc., most welcome!

github.com/llaisdy/Prol...

Is there any simple way to migrate my twitter posts here?