
Pekin Üniversitesi ekibinden iki aşamalı sistem: Cebir sorusunu doğal dilde planlayıp Lean 4 ile kilitlemek
Araştırmacılar, matematiksel strateji üreten bir bileşen ile kanıtı formal dile taşıyan ikinci bir bileşeni birleştirerek büyük dil modellerinin güvenilirlik zayıflığına karşı iki hatlı bir savunma öneriyor. Çalışma ön baskı aşamasında; yine de otomatik teorem kanıtlama ve literatür taramasının bir arada nasıl ölçeklenebileceğine dair somut bir örnek sunuyor.




























