대기열

체커가 하는 모든 일은 한 줄을 거쳐서 이루어집니다. 여기에 있는 것은 시뮬레이션이 아닙니다. 이것들은 지금 상자에 있는 작업입니다.

현재 실행 중

기다리는 중

0 ms

큐를 삭제하기

계산을 위해 주차됨

실행 중

유휴 상태. 이제 제출된 작업은 즉시 시작됩니다.

기다리는 건 없어

한 번에 한 리언 작업만 실행됩니다(Mathlib은 메모리가 많이 필요하며 이 상자는 공유됩니다). 그래서 여러 사람이 한 번에 제출할 때 줄이 생깁니다.

선불 크레딧이 있는 계정은 먼저 서비스됩니다. 이것이 전체 메커니즘입니다. 구입할 별도의 제품이 없습니다. 자유로운 운전은 결코 차단되거나, 억제되거나, 악화되지 않습니다. (단지 앞서 간다) 그리고 여전히 자유로운 레인에서 순서대로 실행됩니다.

이런 방식으로 작동하는 이유는 : 기계를 지원하는 사람들은 다른 모든 사람들이 아무것도 얻을 수없는 수표를 지불하고 있습니다. 줄을 건너 뛰는 것은 유일한 구매하는 것, 그리고 그것은 다른 아무것도 구입하지 않습니다.

도구	결과	찍었어	For
`python`	레이어	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`	레이어	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`	레이어	23.3 s	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`python`	레이어	83 ms	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`pari`	레이어	524 ms	A very-well-poised 7F6 equal to 9Γ(1/3)⁹/64π⁶, via an absolutely convergent Mellin bridge
`pari`	레이어	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	댓글 남기기
`lean`	∎ 확인	15.9 s	댓글 남기기
`python`	레이어	28 ms	댓글 남기기
`lean`	거부됨	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

이 상자의 각 도구의 마지막 20 실행에서 측정, 추정되지 않습니다.