Àwọn àgbèwọlé

Gbogbo àwọn àwọn ìṣàmúlò-ètò tí àwọn ìṣàmúlò-ètò náà ṣè lọ́wọ́lọ́wọ́, àti àwòrán. Kò ní ohunkóhun níbẹ̀ tí jẹ́ ìṣàmúlò-ètò: àwọn àwọn iṣẹ́ nínú àwọn àwọn ààyè-iṣẹ́ nínú àwọn

Ńlá kọ̀ǹpútà

Ìgbà ìtàn

0 ms

to clear the queue

tí a fi pàtó fún ìṣàmúlò-ètò

Ńlà ìṣàmúlò-ètò

Kò ṣiṣẹ́. Àwọn iṣẹ́ tí a fi pamọ́ nígbà yìí tí ń bẹrẹ nígbà.

Tí a bá fẹ́ (0 Àwọn ìṣàmúlò-ètò, 0 Òkù)

Kò ní ohunkóhun tí ǹyàn.

Ààyè àìpẹ̀, àti ohun tí kò jẹ́

One Lean job runs at a time (Mathlib is memory-hungry and this box is shared), so when several people submit at once, there is a line.

Àwọn iroyin àti àwọn ẹ̀yàn àìfilọ́lẹ̀ tí a fi pamọ́ ní ìṣàmúlò-ètò àìfilọ́lẹ̀. Ó jẹ́ gbogbo àwọn àwọn ìṣàmúlò-ètò; kò sí ohun-ìtàn tí a lè ra. Ìjádé ọ̀fẹ́ kò lè gbá, kò lè fí ìjádé silẹ, tabi kò lè fí ìjádé silẹ (kò lè gbá nípa) àti pé o tí n ṣiṣẹ́, ní àwọn ìṣàmúlò-ètò, nínú ààyè ọ̀fẹ́.

The reason it works this way: the people funding the machine are paying for the checks everyone else gets for nothing. Skipping the line is the only thing that buys, and it buys nothing else.

Fi àwọn ìṣàmúlò-ètò ààyè-iṣẹ́ pamọ́ Àwọn àwọn ìṣàmúlò-ètò rẹ

Tí a tí parí

Àwọn Àtòjọ-ẹ̀yàn	Àwọn Àtòjọ-ẹ̀yàn	Tí a fi pamọ́	Fún
`python`	Ìjánú	3.8 s	Au's Conjecture 3.4(a) holds: $\sum_N\dim V_N(S_1)\,t^N=\frac{1}{(1-t)^3(1-t^2)^2}-\frac{t^2}{1-t}$ for the Example II WZ seed
`python`	Ìjánú	1.3 s	Au's Conjecture 3.4(a) holds: $\sum_N\dim V_N(S_1)\,t^N=\frac{1}{(1-t)^3(1-t^2)^2}-\frac{t^2}{1-t}$ for the Example II WZ seed
`python`	Ìjánú	23.3 s	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`python`	Ìjánú	83 ms	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`pari`	Ìjánú	524 ms	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`pari`	Ìjánú	135 ms	$\int_0^1\kappa(x)^2[x(1-x)]^{-2/3}\,dx=\frac{5\sqrt3\,\Gamma(1/3)^9}{2^{11/3}\pi^5}$ , via the CM newform $\eta(3\tau)^8$
`lean`	∎ tí a fi àkóónú	9.2 s	Àwọn Àmì-ìwé
`lean`	∎ tí a fi àkóónú	15.9 s	Àwọn Àmì-ìwé
`python`	Ìjánú	28 ms	Àwọn Àmì-ìwé
`lean`	tí a gbọ́dọ̀	18.9 s	Wrong proof test: 1 + 1 = 3
`lean`	∎ tí a fi àkóónú	30.1 s	Simple verification test: 1 + 1 = 2
`lean`	∎ tí a fi àkóónú	8.4 s	A simple proof, hope it works

Ìgbà wò nínú àwọn ìṣàmúlò-ètò àwọn ìṣàmúlò-ètò

Measured from this box's last 20 runs of each tool, not estimated.

Àwọn Àtòjọ-ẹ̀yàn	Àwọn Ìṣàmúlò-ètò
`lean`	13.7 s
`sage`	15.0 s
`pari`	329 ms
`smt`	22.5 s
`python`	3.2 s
`oeis`	7.5 s
`plot`	15.0 s

Àwọn àgbèwọlé

Ńlà ìṣàmúlò-ètò

Tí a bá fẹ́ (0 Àwọn ìṣàmúlò-ètò, 0 Òkù)

Ààyè àìpẹ̀, àti ohun tí kò jẹ́

Tí a tí parí

Ìgbà wò nínú àwọn ìṣàmúlò-ètò àwọn ìṣàmúlò-ètò

Ṣàfikún àkọlé.

Fi àwọn ìrànwọ́ pamọ́ sí wa