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.

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.