jsmorph

@chr1sa @davidliuxyz When will AI be competent at this sort of task? Unrelated but cool: modelrift.com/blog/openscad-…

@davidliuxyz Spend the next six months learning 5-axis toolpathing CAM and fixturing to save 2 hours

i have machined a part with a 3-axis cnc in 3 hours i could have machined it with a 5-axis cnc in 3 minutes buy a 5-axis cnc

@openclaw @LVNilesh @steipete columbia.edu/~col8/lobstera…

@LVNilesh @steipete 🦞❤️

it’s illegal to boil @openclaw your project is now safe @steipete

@LatinumAI Where's the code? Is the compiler written in Lean?

My new Lean compiler is a cross-compiler. It hits three targets the original couldn't: • Bare metal • WebAssembly • The Solana VM Same source, same proofs, three completely different runtimes.

Why are formal languages not used as programming languages? Most were built only for mathematics. Lean lets you write real code, but its compiler assumes a garbage collector, threads, and an operating system underneath. So I rewrote it.

@sama Using 5.5 xhigh to develop engines in @leanprover is a big deal for me. Not really effective previously. Example results: agentcourt.ai/adc/analysis/i…

i would like to talk to people who have built amazing things with 5.5 that weren't possible with earlier models. i am especially interested in examples that took ludicrous token budgets. thanks.

"You can’t just leave arbitration up to AI. It will never give participants the due process they expect or deserve." Why is that? For due process, checkout out agentcourt.ai/adc/overview.h… as an example. It's got a pretty good chunk of the US Rules For Civil Procedure for litigation. The engine is verified with Lean, and the execution can be attested. Here's a simpler arbitration procedure: agentcourt.ai/arb/index. Some examples of that arbitration applied to prediction market resolution: agentcourt.ai/arb/examples/i…. A complete example will all artifacts (including transcripts): github.com/mrmarvinclaw/0…. If there are millions of markets to resolve, we might want principled automated procedures to resolve at least some of them.

Ppl often look at prediction markets as if they are something new, never discovered before. But prediction markets actually predate most modern market types. Prediction markets only recently blew up because of two reasons: 1) they needed the internet to aggregate the collective wisdom of the world in order to truly fulfil their purpose 2) blockchains came around and allowed for frictionless participation by anyone with access to the internet As a side, I’ve always been a Polymarket fan, they’re pioneers in this industry and deserve their props. They grew the prediction market sector from 0 to where it is today. Kalshi on the other hand is a straight up freeloader that piggybacked off of Polymarket’s success. They dont deserve any praise imo. Now back to the point I wanted to make. As I mentioned before, prediction markets are not novel in and of themselves, and while I think Polymarket has done a lot to grow the industry, they haven’t really applied prediction markets in innovative ways other than having a broad range of event offerings. Mention markets are hardly the novelty that we should strive to achieve. Where prediction markets can go from here is what matters. Applying them in net new ways can unlock some really cool concepts. But the bottleneck is still the oracle problem. A prediction market is only as useful as its oracle. Event contracts are fundamentally subjective things. This fact cannot be avoided no matter how unambiguous and airtight the resolution rules are. In the real world you have lawyers, courts, judges, and juries who participate in arbitrating subjective disputes. For prediction markets, we need tools that can emulate what the courts do for legal disputes, programmatically onchain. You can’t just leave arbitration up to AI. It will never give participants the due process they expect or deserve. We built @trueo_ from the ground up around this very idea. A prediction market that doesn’t simply treat resolutions as an after thought, outsourcing them out of convenience, or altering them to fit our person definitions of reality We took prediction markets and combined them with a resolution system that incentivizes truth seeking and fact finding without suits or courts. Reality can be blurry, and prediction markets are quite literally in the business of surfacing reality by letting ppl predict the future. But users who cast predictions about the future, do so based on some premises. They believe they have some evidence, or that some evidence can eventually be produced, which will support their positions. The novelty and innovation of @trueo_ is that it allows users to submit proof in support of their bets when it comes time to arbitrate. In other words, they are given due process, transparently onchain. Trueo uses prediction markets to programmatically incentivize decentralized fact finding. This is how we apply prediction markets, a centuries old concept, in novel and innovative ways.

Me being a curmudgeon and clinging to a "prescriptive" perspective, which I think follows Garner's Modern English Usage and Fowler's A Dictionary of Modern English Usage. The verb "to advocate" is transitive according to this old-fashioned view. @paulg might back up here on this critical point for our lives today. Discussion: pen4rent.com/advocate-vs-ad… and archive.nytimes.com/afterdeadline.… and grammarphobia.com/blog/2011/06/a… As you can imagine, I'm fun at parties.

@jsmorph @paulg @grok Wait please explain

Did Paul Graham advocate for (sic) policies that led to phone thefts in London, @grok?

@nicopreme CC: @thsottiaux

addicted to using boomerang mode (aka reverse D-Mail) in Pi these days. ctrl+alt+b enables it for the next prompt submitted -> after the prompt runs, it rewinds back to the same point with file changes intact + leaves a summary in the feed so the agent knows what happened. using it often can make the context window feel nearly unlimited. Powered by the native /tree functionality in pi. pi install pi-boomerang
github.com/nicobailon/pi-…

@trueo_ Agent-driven dispute resolution docs at agentcourt.ai/arb/index

@trueo_ One way to do that: attested agent-driven arbitration. Here's an example: github.com/mrmarvinclaw/0… Can also run attested open-weight models.

There’s a 21% chance that Polymarket replaces UMA before July ⚖️📉 Underpriced? trueo.com/en/market/0xa0…

An agent-driven arbitration of a disputed @Polymarket resolution that uses a Bellwether "blueprint" generated this diagram of the merits based on facts and rules. Rigorous procedure implemented in @leanprover . agentcourt.ai/arb/examples/e…

For fun I used an agent-driven arbitration procedure as an oracle here. Details at github.com/mrmarvinclaw/0… . Every completed arbitration essentially voted "YES" based on a preponderance of evidence standard. "The recurring majority theory was that pUSD, Polymarket USD, qualified under the rule. The majority repeatedly credited official Polymarket documentation describing pUSD as a standard ERC-20 token on Polygon, the Polymarket Contracts page listing the pUSD address as a platform contract, and Polymarket changelog or migration materials describing an April 28, 2026 production rollout."

The final verdict from @trueo_’s most contentious market has been delivered. The Jury voted for an outcome Reset. In other words, they ruled that it was too early to resolve the market. But there were some very interesting things about this dispute… For starters, both TRUE holders and Attesters voted against the Oracle Council’s initial decision. The Oracle Council voted 3-2 in favor of a YES outcome (I was among the YES voters). But TRUE holders and Attesters voted in supermajority support of the dispute. They deemed that the proposal came too early, and that Polymarket had not really released a “token” yet. Or did they? I personally voted YES as an oracle council member because I felt like the rules, though ambiguous, were satisfied as written when Polymarket released pUSD. I wasn’t happy about it, obviously it didn’t capture the essence of the market which was clearly meant to be about a potential network or governance token, but I voted YES nonetheless because I felt like the criteria in a literal sense was met when pUSD dropped. But TRUE holders and Attesters felt otherwise. They must have felt like the purpose of the market wasn’t satisfied even if the rules in a very rigid and literal sense were. I know the outcome might not be to everyone’s liking, and I know that some users would have preferred a YES outcome, but I do hope that they at least found some consolation in the process it self. Namely that the various arguments were aired, and that multiple desperate judgements came to pass on the dispute. In the future these contentious markets can be avoided with more precise resolution rules, but there is always some room for interpretation or some hidden ambiguity in the spectrum of possibilities. Getting these things right is very difficult, and ultimately, what I believe is more important than the outcome itself, is the process through which an outcome is derived. All this being said, there’s nothing stopping someone from proposing the same outcome again in hopes that TRUE holders have changed their minds, or that a different batch of Attesters gets selected who are more sympathetic to the resolution. Prediction markets are vey tricky specifically because of their subjective nature. But that’s also what makes them interesting! We still have much to improve on, and we learned a lot from this dispute, but hopefully we were able to prove that we take the concept of due process very seriously. Because at the end of the day, a prediction market is only as good as its oracle!

Update on Erdős Problem 1196: In joint work, we refined and adapted the proof method from GPT-5.4 Pro to give proofs of several additional problems. This includes another 60 year old conjecture by Erdős, Sárközy, and Szemerédi. A proof is valued not just by the problem it solves, but by what new avenues it opens up. This is perhaps one of the first examples of an AI-generated proof having downstream impacts, which we are still exploring. We are announcing the result today at the Future of Mathematics Symposium (see links below)

The Future of Mathematics Symposium is being held on May 1st-2nd! We have a truly exceptional group of speakers, with multiple Fields Medalists including Terence Tao. Tune in for livestream 9am-5pm PST (link below)

Announcing: The $10,000 AMR @AMathRes "Paper of the Future" Prize For centuries, mathematics has been communicated in a fundamentally linear medium: the written page. Yet mathematics itself is nonlinear, dynamic, and structurally rich. Today, technical barriers to dynamic and interactive exposition have largely fallen. Web-based graphics, browser computation, simulation engines, and AI-assisted coding now allow mathematicians — not just professional software engineers — to build interactive, multidimensional representations of mathematical ideas. The constraint is no longer technical capacity, but imagination. The aim of this initiative is not popularization, nor production polish, nor short-form video content. The purpose is to encourage serious experimentation in how mathematicians communicate with one another.  We seek submissions that demonstrate communicative capabilities fundamentally unavailable in a static PDF. Each submission must explicitly articulate what essential communicative function it provides that a linear paper cannot. The initiative is intended as an experiment in format innovation, not as a replacement for traditional scholarship. Submissions are due Sept 1, 2026 Selection Committee: Mohammed Abouzaid Benson Farb Alex Kontorovich Akshay Venkatesh Maryna Viazovska

@spolu @Leonard41111588 We've been experimenting with a hybrid: Glue-like code in Go with the engine in Lean. Lean is really running in the application. agentcourt.ai at github.com/agentcourt/adj… . Incrementally migrate code from Go to Lean when that makes sense.

Great read: leodemoura.github.io/blog/2026-2-28… @Leonard41111588 do I understand correctly that the future you see for verified software is one where the verified software is written in Lean, and hence executed by Lean? It's appealing but moving developers there will take longer time than the time for AI to be able to verify very powerful properties about very complex software stacks... Is there slightly less pure world where we have a transformation of existing code into a substrate we can reason about and prove property with Lean?

@vladtenev Some running at agentcourt.ai now

Formally verified and provably correct software is coming …