13,553 karma · joined April 8, 2011
> Coder: a coding version with half of the experts removed. It reaches 91% of the full model's SWE-bench Verified score (measured by its authors) and fits 32 GB of RAM.
https://github.com/Niko1221/Strata#which-model-should-i-pick
<script>
let count = $state(0);
let dialog;
</script>
<button
onclick={() => {
count++;
dialog.showModal();
}}
>
:)
</button>
<dialog bind:this={dialog}>
<p>
Hello, I was clicked {count} times
</p>
<form method="dialog">
<button>Close</button>
</form>
</dialog>
The inline onclick handler doesn't seem super readable, but the rest is fine.Not sure why you wouldn't want to preserve timestamps, links, etc. by default.
> Alexander, originally from the Greek Ἀλέξανδρος (Aléxandros), from αλέξειν aléxein meaning "to ward off, keep off, turn away, defend, protect" and ἀνδρός andrós, genitive of ἀνήρ anḗr meaning "man".
> Meaning "Defender, protector of man"
For the rest of the world, it's about 222m.
> objects the size of monster truck tires
FFS, just use metric! Apparently that's about 1.7m.
Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theorem being verified is what you think. And of course a lot of maths can't yet be expressed in Lean as the foundations haven't been built up enough.