Partida publikoak
Argitaratutako exekuzioak, panelak barrara iritsi ezin izan zuena barne. Emaitza hori da gakoa: Lean kernelak ukatzen duen formalizazio batek argumentua inoiz justifikatu ez den pauso zehatza adierazten dizu.
Hemengoa
Gune hau lan deduktiboetarako sortu da: matematika hutsa eta aplikatua, logika, informatika teorikoa, fisika teorikoa eta teoria ekonomikoa — esperimentuaren ordez frogapenaren bidez ebazten diren argudioak. Galderak enpirikoetarako, zintzoa den epaia teorema bat baino bilaketa bat den kasuetan, erabili gure referee.chat gunea.
Joan referee.chatra