persedes
Joined 6 years ago
Joined 6 years ago
Try this, it uses a tax engine as the backbone and provides feedback for Claude if it goes off the rails. Albeit it doesn't support every tax scenario.
the FDA wanted data from organs-on-a-chip or some comparable alternative.
This is the main takeaway from the article imho and great news! ~15 years ago those systems were were not very interesting for pharma companies (bayer used to have a campus a few s-bahn stops away) due to regulators requiring animal tests over those systems.However this week spent an hour with claude to migrate to tailscale, latest home assistant update, sensor setup and filtering for my rtl433 antenna, connected hue lights while we're at it, migrated to latest pihole version and put everything in git in one nice compose file with a step by step instruction on how everything was setup and which account sign ups were needed. I still checked every step and manually approved stuff, but the remote session feature made this easy to finish.
> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That's exactly what the navier stokes paper posted yesterday pointed out where the LLM bends the Lean code to make it "compile", because the NL might be wrong to begin with or because it missed a detail:https://arxiv.org/html/2610.08144v1#S2
For complex / tedious proofs I can easily see how small details like this can lead to a valid lean proof (or valid "code"), but missing the important details that got lost.
https://github.com/hiroppy/tmux-agent-sidebar
Has been pretty nice