Dirije avètisman an. Kernel la deside si li ka pwouve.

Yon panel de modèl atak pwoblèm ou ak literati, SageMath, PARI/GP ak yon SMT solver, Lè sa a, fòmalize rezilta nan Lean 4 kont Mathlib. Lean' s kernel oswa aksepte prèv la oswa li pa, epi pa gen kantite lajan nan konfidans pwosè chanje sa. Lè li pa travay ou jwenn objektif egzak ki rete, ki se anjeneral kote argument informal te hand- waving.

Objektif

Se yon bagay ki klè sou sa done vle di. 'Decide si X se vre, epi montre li' bat 'di m' sou X'.

Bar li dwe netwaye

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

Arbitre a kenbe bar sa a literalman. Mande pou yon prèv nivo prim e li pral di ou klèman lè panèl la pa rive, piske li pa deklare viktwa.

Panèl la

Pi gwo kantite sijè vle di plis ang, ak plis pri pou chak ranje.

Arbitre

Règleman sou kritè yo ak re-verifye chak pati nan prèv. Vale a ou pi fò modèl.

Rounds

Limit depans

Si ou klike li, match la pral an pauze. Pa gen anyen ki pèdi.

Vizibilite

Piblike lè fini

Enskri pou kòmanse yon match

Kont nouvo yo resevwa kredi kòmanse, ase pou yon match reyèl.

Yon chèchè ki pa ka konfonn

Lean 4 ak Mathlib kalite-cheke deklarasyon final la, ak yon prèv ki leaned sou sorry, native_decide oswa yon axiome fre se refize pi plis pase konte. Avèk li: SageMath, PARI/GP, Z3, CVC5 ak OEIS, se konsa yon konstriksyon ka dwe konpile ak idantifye anvan nenpòt moun ki eseye pwouve nenpòt bagay sou li.

Yon prèv ki pa travay se yon rezilta

Lè fòmalizasyon an pa reyisi, objektif Lean pa t 'kapab fèmen se bay nenpòt ki sijè ki pi byen plase pou atak li: sèlman objektif sa a, pa tout istwa a. Yon prèv refize non diferans lan egzakteman, ki se plis pase pi fò nan arguments informels janm fè.

Pa gen anyen ki pwouve de fwa

@ info