BlueberryWren은 유클리드의 소수 무한성 증명을 Isabelle/HOL, Lean, HOL4, Agda로 구현해 자동화와 편집 경험을 비교했다. 이번 작업에서는 Isabelle/HOL과 HOL4의 정리 검색과 자동화, Lean의 대화형 상태 표시가 유용했고 Agda는 직접 증명 항을 구성하는 부담 대신 계산 가능한 증명을 제공했다. 관련 토론에서 작성자는 Lean 전술도 내부적으로 증명 항을 만든다고 보완했다. 도구별 숙련도가 다른 단일 과제이므로 객관적인 우열 평가와는 구분해야 한다.