Жасау, тек қайта үлгілеу емес: Lean 4-тегі шектеулі компиляторға негізделген жөндеу
arXiv:2610.26942v1 Жариялау түрі: жаңа Анықтама: Автоматты теорема дәлелдеушілер жиі тіл моделін үлгілеуге таянады, бірақ Lean сияқты дәлелдеу көмекшілері әр қате қадамды дәл қате хабарламасымен қате деп есептейді — бұл ақпарат тек үлгілеуден бас тартады. Бұлды шешу үшін біз...