IsabeLLM, автоматизированная система доказательства теорем в Isabelle, интегрирует архитектуру усиленного извлечения и генерации, отслеживание ошибок и генерацию контрпримеров для расширения контекста для больших языковых моделей. Обновленная версия демонстрирует улучшенную производительность при проверке протокола Proof of Work в Bitcoin по сравнению с оригинальной версией.