Legg i kø

Alt sjekkerne gjør går gjennom en kø, og dette er det. Ingenting her er en simulering: dette er jobbene på boksen akkurat nå.

kjører nå

venter

0 ms

for å tømme køen

parkert for beregning

Kjører

Tomgang En jobb som er levert starter nå med en gang.

Venter (0 priority, 0 ledig)

Ingenting venter.

Den raske kjørebanen, og hva det ikke er

En Lean jobb kjører samtidig (Mathlib er minne-hungre og denne boksen er delt), så når flere folk sender inn samtidig, så er det en linje.

Alle kontokontoer med forhåndsbetalt kreditt ytes først. Det er hele mekanismen, det er ingen egen vare å kjøpe. en fri kjøring blir aldri blokkert, gasset eller forringet av den (bare overhalet) og den kjører fortsatt, i orden, i den frie kjørebanen.

Grunnen til at det fungerer på denne måten: folkene finansierer maskinen betaler for sjekkene alle andre får for ingenting.

Legg til godskriving for å hoppe over linja Beregner du

Nylig ferdig

Verktøy	Resultat	Tok	Til
`python`	løpt	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øpt	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øpt	23.3 s	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`python`	løpt	83 ms	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`pari`	løpt	524 ms	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`pari`	løpt	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`	verifisert	9.2 s	en kommentar
`lean`	verifisert	15.9 s	en kommentar
`python`	løpt	28 ms	en kommentar
`lean`	avvist	18.9 s	Wrong proof test: 1 + 1 = 3
`lean`	verifisert	30.1 s	Simple verification test: 1 + 1 = 2
`lean`	verifisert	8.4 s	A simple proof, hope it works

Hvor lenge hver sjekker vanligvis varer her

Målt fra de siste 20 seriene av hvert verktøy, ikke beregnet.

Verktøy	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

Legg i kø

Kjører

Venter (0 priority, 0 ledig)

Den raske kjørebanen, og hva det ikke er

Nylig ferdig

Hvor lenge hver sjekker vanligvis varer her

Bli med i samtalen.

Send tilbakemelding