Hacker News

Top stories

Live mirror
30 storiesupdated just nowView source snapshot
  1. One Year of Sponsored Servo Development(servo.org ↗)
    54comments
  2. Neovim have a ~$800k Bitcoin donation sitting untouched since 2023
    21comments
  3. Nvidia announces native GPU programming in Rust(nvidia.com ↗)
    304comments
  4. My temporary PHP fix from 2014 has nearly 20M installs. Today I'm deprecating it(jakeasmith.com ↗)
    37comments
  5. Keys Not Included: recovering the signing keys for US driver's license barcodes(ryan.science ↗)
    72comments
  6. GLM Built Its Own Inference Infrastructure(z.ai ↗)
    74comments
  7. The Relation Between Mathematics and Physics by Paul Dirac(cam.ac.uk ↗)
    24comments
  8. Training a 4B model to produce 81% faster query plans than Postgres(rohanbansal.com ↗)
    121comments
  9. Better Vector Search for Long Documents: Chunking Inside Manticore Search(manticoresearch.com ↗)
    discuss
  10. OpenAI Model Misalignment Report(openai.com ↗)
    43comments
  11. Iran school bombing: grounds to believe US was behind atrocity, UN finds(theguardian.com ↗)
    1comments
  12. Online Z3 Guide(microsoft.github.io ↗)
    6comments
  13. Lucasart's Afterlife(togameforlife.wordpress.com ↗)
    18comments
  14. Xiaomi Mimo 2.6 live post-training dashboard(xiaomi.com ↗)
    122comments
  15. Small programming tricks(will-keleher.com ↗)
    243comments
  16. Comparison of Malloc() Algorithms(egbert.net ↗)
    18comments
  17. Backups Aren't Simple(filipovski.net ↗)
    160comments
  18. Developing provably correct Rust code with Verus(amazon.science ↗)
    22comments
  19. Breaking the 1.58-bit Barrier for Ternary LLMs(arxiv.org ↗)
    34comments
  20. Cloudflare/Security-Audit-Skill(github.com/cloudflare ↗)
    16comments
  21. Show HN: An e-ink frame that hears birds and draws them as 1800s illustrations(github.com/arnegiacomo ↗)
    245comments
  22. A 32-year-old bug walks into a Telnet server(watchtowr.com ↗)
    28comments
  23. AWS says it can't restore some data from mideast facilities struck by Iran(wsj.com ↗)
    363comments
  24. HarnessTax: How Much Does the Harness Matter for Coding Agents?(harnesstax.github.io ↗)
    55comments
  25. The engineering behind the US Strategic Petroleum Reserve(johnjwang.com ↗)
    88comments
  26. Performance Improvements in .NET 11(devblogs.microsoft.com/dotnet ↗)
    78comments
  27. PCB is brought to you by Fable 5(a6mzero.com ↗)
    58comments
  28. OpenSpec – A lightweight and configurable AI spec framework(openspec.dev ↗)
    69comments
  29. The Return of Sail Power: Cargo Ships Are Turning Back to the Wind(gcaptain.com ↗)
    72comments
  30. Japan's book scene is moving from bookstores to libraries(untranslatedjp.substack.com ↗)
    82comments

Online Z3 Guide

16 pointsby 1d agomicrosoft.github.io
6 comments
1h agoHN ↗

If anyone wondering, because it took me a few hops to find out:

Z3 is a high-performance theorem prover being developed at Microsoft Research.

53m agoHN ↗

Or a BMW, or a groundbreaking electro mechanical computer, depending :)

41m agoHN ↗

oh, something new! I thought Z3 is SAT/SMT solver, they must have added something.

40m agoHN ↗

Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.