throwalean
No user record in our sample, but throwalean has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
No user record in our sample, but throwalean has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
"Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.
Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-; Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138