frontpage.
newsnewestaskshowjobs

Made with ♥ by @iamnishanth

Open Source @Github

fp.

Show HN: FFmpeg WebCLI – Full FFmpeg in Browser, Offline PWA, No Uploads(WASM)

https://github.com/tejaswigowda/ffmpeg-webCLI
63•tejaswigowda•3h ago•18 comments

Show HN: Mercek – A Desktop IDE for AWS ECS

https://www.mercek.dev/
13•utibeumanah•2h ago•0 comments

Show HN: Papernews – self-hosted daily newspaper PDF for your reMarkable

https://github.com/marcj/papernews
2•bourbonproof•18m ago•0 comments

Show HN: Hitoku Draft – Context aware local assistant

https://hitoku.me/draft/
8•lostathome•5h ago•0 comments

Show HN: Uruky (EU-based Kagi alternative) now has Image Search and URL Rewrites

https://uruky.com/?il=en
205•BrunoBernardino•14h ago•190 comments

Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

https://github.com/schildep/verified-polygon-intersection
31•permute•1h ago•5 comments

Show HN: Cost.dev (YC W21) – making agents cost-aware and cheaper to call

https://cost.dev/
25•akh•12h ago•9 comments

Show HN: Prela – Purely Algebraic Relation Combinators

https://github.com/remysucre/prela
59•remywang•3d ago•13 comments

Show HN: A native port of Skate 3 for Windows & Linux via static recompilation

https://github.com/mchughalex/skate3recomp
3•turingfeel•1h ago•0 comments

Show HN: NoiR Code – because QR sounds similar to "noir"

https://noir-code.suncake.xyz/
4•Sunkek•1d ago•1 comments

Show HN: Using Haskell to play music on 3D printer motors (2020)

https://lucasoshiro.github.io/software-en/2020-07-31-music_gcode/
6•lucasoshiro•3h ago•1 comments

Show HN: Boxes.dev: ditch localhost; run Claude Code and Codex in the cloud

https://boxes.dev
81•nab•9h ago•61 comments

Show HN: Edsger – A handwritten Clojure REPL for the reMarkable 2

https://handwritten.danieljanus.pl/2026-06-01-edsger.html
253•nathell•2d ago•34 comments

Show HN: Bot or Not – Spot AI-generated randomness

https://play-bot-or-not.vercel.app/
4•EvanZhouDev•3h ago•0 comments

Show HN: I reverse-engineered the world maps of Test Drive III (1990 DOS game)

https://github.com/s-macke/Test-Drive-3-Maps
213•s-macke•4d ago•55 comments

Show HN: Digger Solo – Local AI File Explorer

https://solo.digger.lol
3•sean_pedersen•4h ago•0 comments

Show HN: Wallflower.app – A Combined Mastodon and Bluesky Client

https://thewallflower.app
2•tldrthelaw•2h ago•0 comments

Show HN: Nutrepedia – Nutrition info in 29 locales built with Clojure and Htmx

https://nutrepedia.com/en-us/
128•llovan•1d ago•28 comments

Show HN: Mnemo – local-first AI memory layer for any LLM (Rust, SQLite,petgraph)

https://github.com/zaydmulani09/mnemo
54•zaydmulani•1d ago•25 comments

Show HN: Eyeball

https://eyeball.rory.codes/
287•mrroryflint•2d ago•86 comments

Show HN: Bit-banged 10BASE-T Ethernet and Wi-Fi router in Rust on the Pico 2 W

https://github.com/mattdeeds/pico-10base-t-rs
5•mdeeds•8h ago•0 comments

Show HN: Bio Glyph – Turn Your Face into a One-Line Drawing

https://bio.bairui.dev/
19•subairui•23h ago•14 comments

Show HN: AgentKitten: Swift package for provider-agnostic AI agents

https://github.com/fbeeper/agentkitten
10•fbeeper•9h ago•1 comments

Show HN: ClearLogo – a logo API that returns usable logos, not raw files

https://clearlogo.dev/en
6•ehalim•9h ago•2 comments

Show HN: Rscrypto, pure-Rust crypto with industry leading public benches

https://github.com/loadingalias/rscrypto
32•LoadingALIAS•1d ago•14 comments

Show HN: Live breath detection and biofeedback from a phone microphone

https://github.com/shiihaa-app/shiihaa-breath-detection
64•felixzeller•2d ago•25 comments

Show HN: Ideogram 4.0 – open-weight 9.3B text-to-image model

https://github.com/ideogram-oss/ideogram4
44•pigcat•1d ago•10 comments

Show HN: Hydron – Hardware-aware coding agent

https://www.hydron.sh/
8•prashantsengar•10h ago•7 comments

Show HN: Lint Your Markdown with ESLint

https://github.com/lumirlumir/npm-eslint-markdown
14•beenzinozino•1d ago•3 comments

Show HN: RePlaya – self-hosted browser session replay with live tailing

https://github.com/s2-streamstore/replaya
50•shikhar•2d ago•8 comments
Open in hackernews

Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

https://github.com/schildep/verified-polygon-intersection
31•permute•1h ago
To my knowledge, this is the first formally verified implementation of an intersection algorithm for polygons.

The experience of working with AI agents on this project changed a lot with recent model releases, as I describe in the readme. Opus 4.8 is able to provide algorithm implementation with formal proof in one shot, whereas previous models required me to provide proof strategies in multiple steps.

Trust in the correctness comes entirely from the Lean checker and human review of a small specification, not from the LLM.

Also check out the web demo built around the verified core linked in the readme: https://schildep.github.io/verified-polygon-intersection/. It supports multipolygons including holes, self intersections, and overlapping edges.

Comments

CyLith•1h ago
Does this use integer coordinates or floating point coordinates?
threatripper•1h ago
It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...
porcoda•12m ago
I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).
olaird25•48m ago
Is the web demo compiled from the lean?
prewett•17m ago
This is a great use for AI! Calculating intersections is tedious and there are an surprising number of edge cases that are tedious to track down and fix.