Kø
Alt hvad brikkerne gør går gennem en kø, og det er det. Intet her er en simulation: dette er job på kassen lige nu.
Kører
Et job, der er blevet indsendt, begynder nu.
Venter (0 prioritet, 0 fri)
Intet venter.
Den hurtige bane, og hvad det ikke er
Et Lean job kører ad gangen (Mathlib er hukommelses-hunger og denne boks deles), så når flere mennesker indsender på én gang, er der en linje.
Enhver konto med forudbetalt kredit serveres først. Det er hele mekanismen; der er ikke noget separat produkt at købe. En gratis kørsel er aldrig blokeret, trummeret eller nedbrudt af det (kun overhalet), og det kører stadig, i orden, i fri bane.
Grunden til at det virker på denne måde: folk finansierer maskinen betaler for de kontroller, alle andre får for ingenting. Spring linjen er det eneste, der køber, og det køber intet andet.
Lige færdig
| Værktøj | Resultat | Tog | For |
|---|---|---|---|
python |
løb | 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 |
løb | 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 |
løb | 23.3 s | A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge |
python |
løb | 83 ms | A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge |
pari |
løb | 524 ms | A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge |
pari |
løb | 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 |
, | 9.2 s | en kommentar |
lean |
, | 15.9 s | en kommentar |
python |
løb | 28 ms | en kommentar |
lean |
afvist | 18.9 s | Wrong proof test: 1 + 1 = 3 |
lean |
, | 30.1 s | Simple verification test: 1 + 1 = 2 |
lean |
, | 8.4 s | A simple proof, hope it works |
Hvor lang tid hver checker tager normalt her
Målt fra denne bokss sidste 20 løb af hvert værktøj, ikke anslået.
| Værktøj | Typisk |
|---|---|
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 |