Hacker News

Top stories

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

Online Z3 Guide

27 pointsby 1d agomicrosoft.github.io
6 comments
2h 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.

1h agoHN ↗

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

1h agoHN ↗

I was hoping for the mechanical computer...

1h agoHN ↗

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

1h 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.