世間では、自然言語で会話できるチャットAI／大規模言語モデルの話題が盛り上がってますが、僕にとっての当面の期待は、人間可読でありながら機械可読でもある形式的証明記述の可能性です。長年のストレスであった次のジレンマが解決するかも知れません。 機…