Wysuń roszczenie. Jedro decyduje, czy jest udowodnione.

A panel of models attacks your problem with the literature, SageMath, PARI/GP and an SMT solver, then formalises 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.

Cel

"Decydź, czy X jest prawdą, i udowodnij, że to jest "przekonaj mnie o X".

Bar, który musi oczyścić.

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.

Sędzia dosłownie posiada ten bar. Poproś o dowód na poziomie nagrody i to wyraźnie powie ci, kiedy panel upadnie, zamiast ogłosić zwycięstwo.

Panel

Więcej miejsc oznacza więcej kątów i więcej kosztów w jednej rundzie.

Prezes

Zasady dotyczące kryteriów i ponowne sprawdzanie każdego dowodu warte twojego najsilniejszego modelu.

Rundy

Limit wydatków

Wciskanie zatrzymuje zapałkę.

Widoczość

Opublikuj po zakończeniu

Zarejestruj się, aby rozpocząć pasowanie

Nowe konta zaczynają się odliczać, wystarczy na prawdziwą zgodę.

Kontroler, którego nie można przekonać

Lean 4 with Mathlib type-checks the final statement, and a proof that leans on sorry, native_decide or a fresh axiom is rejected rather than counted. Alongside it: SageMath, PARI/GP, Z3, CVC5 and the OEIS, so a construction can be computed and identified before anyone tries to prove anything about it.

Nieudany dowód to odkrycie

Kiedy nie uda się formalność, cel Lean nie mógł zamknąć jest przekazany do miejsca, które jest najlepsze, aby go atakować: tylko ten cel, nie cała historia. Odrzucony dowód nazwą luki dokładnie, co jest więcej niż większość nieformalnych argumentów kiedykolwiek robią.

Nic nie jest udowodnione dwa razy

Każda lema, która utworzy panel, wchodzi w wspólną księgę z dowodem, więc nigdy nie jest ponownie pochodzący i martwe zaułki nigdy nie są ponownie próbowane. Długie problemy zatrzymują się i nie tracą pracy: zamknij kartę i wróci jutro.