MLフレームワーク*をLeanで書き直しました（そして、より高速になりました*）

tinygradは、機械学習の小規模フレームワークとして知られるオープンソースプロジェクト。開発者のGeorge Hotz（ジョージ・ホッツ、通称geohot）が率いる。最小限のコードでニューラルネットワークの訓練・推論を可能にし、PyTorchのサブセット的な位置づけ。 Leanは、Microsoft Researchが開発した定理証明支援系および関数型プログラミング言語。通常のAI/ML開発にはPythonとCUDAが使われるが、Leanは数学的証明の検証に強みを持つ。今回のプロジェクトは、tinygradのコア部分をLeanで書き直すという試みで、性能が向上したと主張。 このブログ記事は、形式検証（formal verification）と実用的な機械学習フレームワークの接点を探る実験的プロジェクトの成果報告。単なる「書き直し」ではなく、Leanの持つ最適化能力や証明の仕組みを活用することで、従来のPython実装より高速になった点が注目されている。AI/ML業界では「Rustで書き直す」ブームがあるが、さらに先を行く話題として受け止められている。