Public matches
Published runs, including the ones where the panel could not reach the bar. That outcome is the point: a formalisation the Lean kernel refuses tells you exactly which step the argument never justified.
What belongs here
This site is built for deductive work: pure and applied mathematics, logic, theoretical computer science, theoretical physics and economic theory — claims that are settled by proof rather than by experiment. For empirical questions, where the honest verdict is a finding rather than a theorem, use our sister site referee.chat instead.
Go to referee.chat