Lean v4.35.0 versiyasida mantiqiy to'g'riligi isbotlangan yangi yadrolar taqdim etildi

Lean v4.35.0 versiyasi lake check buyrug'i hamda to'rtta yangi yadro bilan chiqarildi. Ular orasidagi con-leche yadrosi Lean tilida yozilgan bo'lib, uning mantiqiy to'g'riligi Claude modeli va Joachim Breitner tomonidan isbotlangan.

Shuningdek, Rust tiliga o'tkazilgan hamda Aeneas vositasi orqali tekshirilgan con-ron yadrosi ham ushbu versiyaga qo'shildi. Ishlab chiquvchilar yaqin oylarda uchinchi tasdiqlangan lean4lean yadrosini ham yakunlashni rejalashtirishmoqda.

Oddiy AI texnologiyasi yordamida tarjima qilingan