1 source filed · JA 1
Scope: income tax, corporate tax, local taxes, consumption tax and items such as depreciation; only pure calculation functions whose inputs are explicit arguments.
76,165distinct inputs on which production Ruby and its Lean copy were compared for the income-tax rate table, with 0 mismatches
1 source filed · EN 1
Main theorem: #k-SAT on n variables and m clauses is solvable in time 2^O(min{k²n log log n/√log n, km/√log m}), using tensor networks and rank arguments plus count-preserving sparsification.
800papers found that prove at least one result only under ETH or a hypothesis implying it (more than 800)
1 source filed · EN 1
Approach: compile library plus fuzz test to RISC-V; combine with Theorem's RISC-V and Linux process semantics and a no-crash property to yield a spec; Claude writes the proof; Rocq checks it.
239OSS-Fuzz entry points proved never to crash for inputs under 64 MB
1 source filed · EN 1
Two kinds of autoformalisation: (i) turning a proof into any Lean proof that compiles; (ii) faithfully translating every statement and argument.
m+4 vs m+5derivatives required in OpenAI's paper (eq. 8.19) versus in the cited Lean theorem