Наведи го тврдењето.

Панел од модели го напаѓа вашиот проблем со литературата SageMath, PARI/GP и SMT решавачот, потоа го формализира резултатот од Lean 4 против Mathlib. Јадрото на Lean или го прифаќа доказот или не го прифаќа, и не се менува тоа со никаква самодоверба во прозата. Кога не ја добивате точната цел која останува, која обично е каде што неформалниот аргумент беше рачно таласање.

Целта
Биди прецизен за тоа што значи. 'Одлучи дали X е точно, и докажи дека е подобро од 'речи ми за X'.
Барот кој мора да го исчисти.
Барајте доказ на ниво на наградата и ќе ви каже кога панелот ќе пропадне, наместо да прогласи победа.
Таблата
Повеќе места значи повеќе агли, а повеќе цена за круг.
Судија
Правилата за критериумите и повторно ги проверуваат сите докази.
Раунди
Ограничување на трошоците
Ако го запреш, ќе ги паузираш match.
Видливост
Запиши се за да започнеш match
Новите сметки се заработуваат, доволно за вистински match.
Да.

Lean 4 со Mathlib тип- го проверува конечниот израз и доказ кој се потпира на sorry, native_decide или свеж аксиом се отфрла наместо да се преброи. Покрај него: SageMath, PARI/GP, Z3, CVC5 и OEIS, за да може да се пресметува и идентификува изградбата пред некој да се обиде да докаже нешто за тоа.

Неуспешен доказ е пронаоѓање

Кога формализацијата не успеа, целта Лиан не можеше да ја затвори е предадена на кое место е најдобро за да се нападне: само таа цел, не целата историја.

Ништо не е докажано двапати

Секоја лема на панелот оди во заедничка книга со нејзиниот доказ, така што никогаш не е повторно изведена и ќор-сокак никогаш не се повторуваат. Долгите проблеми застануваат и продолжуваат без да губат работа: затвори го ливчето и врати се утре.