Kutaura chikumbiro. Kernel inofunga kana ichiratidza kuti chikumbiro chacho chakakodzera.

A panel of models attacks your problem with the literature, SageMath, PARI/GP and a SMT solver, then formalizes the result in Lean 4 against Mathlib. Lean's kernel either accepts the proof or it does not, and no amount of confident prose changes that. When it fails you get the exact goal that remains, which is usually where the informal argument was hand-waving.

Chinangwa
Kuziva kuti zvaitwa zvinoreva sei. 'Decide whether X is true, and prove it' beats 'tell me about X'.
Iyo bar iyo inofanira kubvisa
Kubvunza proof yemari-level uye ichakuudza zvakajeka kana pane imwe panel ikasaenda kure, kupfuura kuzivisa kukunda.
Pane
Mamwe mabheji anoreva ma Angles akawanda, uye mari yakawanda pa round.
Mutongi
Ruzivo rwezviyero uye kuongororazve kwese kwese kwechokwadi. Kubhadhara yako yakasimba kwazvo model.
Rounds
Kubhadhara
Kukanda kunoita kuti match iite pauses. Hapana chinorwadza.
Kuonekwa
Sign up to start a match
New accounts get starting credit, enough for a real match.
A checker that cannot be persuaded

Lean 4 ne Mathlib type-cheka yakati chirevo, uye kuratidza kuti inotarisa pa sorry, native_decide kana atsva axiom yakasungwa kupfuura kunyorwa. Pamusoro pa: SageMath, PARI/GP, Z3, CVC5 uye OEIS, saka kugadzira anogona kuongororwa uye kuzivikanwa pamberi munhu wese anozviedza kuratidza chero chinhu pamusoro apa.

A failed proof is a finding

Kana formalization kukundikana, chinangwa Lean aigona kwete kugara yakapihwa kune chero chigaro zviri nani kuiswa kuuraya: chete kuti chinangwa, kwete zvese nyaya. A yakasungwa proof mashoko chigaro zvakajeka, izvo zviri kupfuura zvakawanda zvisina pamutemo mashoko nguva dzose kuita.

Hapana chinoratidzwa kaviri

Every lemma paneli inogadzira inoenda muchikamu chekugoverana nechokwadi, saka haisi kudzokera ku-kubva uye matambudziko haasati adzokera. Long nyaya kusvikira uye kuenderera mberi pasina kushaya basa: bvisa tab uye tarisazve nezuro.