frunkp

Makes me want to browse the same for maths researchers with Erdos number.

I know Grigori Perelman is far from Erdos, which is fun :)

Can anyone confirm that they are also "Gentle Llama" on Mullvad browser?

I just installed it, I want to know if everyone gets the same hash (same identity for everyone).

When I saw "hidden reasoning", it reminded me of diffusion models: generating a block spans many steps (with remasking), which hide the reasoning that led to the block.

I had not heard of looped transformers, but the engineering behind the number of loops per token / halting feels like trying to apply a diffusion process to a transformer while keeping the auto-regressive feature.

Those who play go may enjoy the variants: https://www.govariants.com/variants/rules-list Tetris is a fun one to try!

The model does well on highschool competition maths. Problems in the "Set Theory" and "Natural Numbers" chapters of Elements of Abstract Algebra may be doable with Kimina-Prover, nothing beyond because it doesn't know Sylow theorem etc. and hasn't used these objects with Lean 4 in practice.

You can start with a natural language description of the theorem: demo.projectnumina.ai and an autoformalizer will generate the formal statement. It's an additional click of a button to have it attempt to prove it.

For natural language interpretation of Lean proofs, the current LLMs (o4-mini-high, Claude 4, Gemini 2.5 Pro) do a decent job of walking you through.