Amazon с помощью ИИ доказала надёжность протокола базы данных Aurora
Языковая модель написала математическое описание протокола Aurora и доказательство его надёжности, их проверила программа для математических доказательств Lean 4, а в документации нашлись опасные неточности.