Ciro Santilli @cirosantilli 37

The beauty of Project Euler is that it would serve both as a AI code generation benchmark and as an AI Math benchmark!

Bibliography:

"Autoformalization" refers to automatically converting a traditional human readable mathematical proof to a formal proof.

The topic received some attention with the AI boom and rise of LLMs:

By Princeton people.

This one aims to solve GitHub issues. It appears to contain 2,294 real-world GitHub issues and their corresponding pull requests

The dataset appears to be at: huggingface.co/datasets/princeton-nlp/SWE-bench in Parquet format.

We define an "Inscription service" as a website that easily allows you to pay to have arbitrary data inscribed on a blockchain.

The most notable early example of such a service on the Bitcoin blockchain was cryptograffiti.info.

We define an "inscription system" as a software or service that facilitates the creation of inscriptions.

Author of Infinite Napkin.

Profiles:

He's also a mathematical olympiad coach.

The cool thing about Terrence Tao is that besides being a mathematical genius, he is also interested in modern technology such as formal proof systems (notably Lean), automated theorem proving and forum-like collaboration as in MathOverflow^[ref]. For that, huge kudos.

Impossible without expect? Fuck...

Attempt at: ollama-expect

TODO: haven't managed. /set parameter seed 0:

Across hardware:

It might be easier to just use llama-cli for this, it has a --temperature flag.