Lightnews — Scholar-powered news

iamwil @interjectedfuture.com · 18h

Likely! The definition of abelian groups is already in standard lib. But this was for learning. Also, one thing I didn’t mention was that Lean 4 doesn’t do tree shaking, so if you pull in the standard lib, it ballon’s the compiled C executable from ~9MB to ~140MB.

Reposted by iamwil

brennan @brennan.computer · 23h

incidentally, this is how I learned everything in 3D

I had an image I wanted to make, and no idea how to get from A to Z, but you just start stumbling through stuff and learn a bit of B or C, or a bit of LMNOP and then back to E or F, and suddenly it starts resolving, solidifying out of the fog

iamwil @interjectedfuture.com · 1d

The old path: Learn Lean (6 weeks), study abstract algebra (8 weeks), understand group theory (4 weeks), finally attempt your proof.

The new path: Start with your exact problem. Generate a tutorial for it. Backfill concepts as you hit them.

1 2 5

Reposted by iamwil

dan @danabra.mov · 1d

this is the way to learn with ai. you can start anywhere and backfill. you have to remain curious and careful and not just passively eat up plausible explanations. but if you put in the effort and the model is good, it’s powerful

iamwil @interjectedfuture.com · 1d

The old path: Learn Lean (6 weeks), study abstract algebra (8 weeks), understand group theory (4 weeks), finally attempt your proof.

The new path: Start with your exact problem. Generate a tutorial for it. Backfill concepts as you hit them.

2 4 43

iamwil @interjectedfuture.com · 1d

Read the full article for the details. If you like using AI to learn (among other topics), you should subscribe to my blog.

interjectedfuture.com/the-best-wa...

The Best Way to Learn Might Be Starting at the End: Writing a Proof in Lean

AI leveraged learning lets you start with the application at the end. Curiosity guides what you learn, fundamentals backfill when you need them.

interjectedfuture.com

3

iamwil @interjectedfuture.com · 1d

Try it: “Generate a Lean 4 tutorial for proving Z-sets over additive merge form an abelian group.”

Here's a copy of my proof: gist.github.com/iamwilhelm/...

Proof that Z-set and additive merge form an abelian group

Proof that Z-set and additive merge form an abelian group - zset_abelian.lean

gist.github.com

1 1

iamwil @interjectedfuture.com · 1d

You can learn by diving into projects you care about, starting from the end, and backfilling the fundamentals as you go. No longer do you need to wait to get started on the fun stuff.

1 1

iamwil @interjectedfuture.com · 1d

The bridge exists now where there was none before. Adjacent tools, languages, and ecosystems are within reach.

Formal verification becomes a practical tool for backend engineers, not “PhD territory.” This can expand out to other programming subgenres, and even other STEM fields.

1 3

iamwil @interjectedfuture.com · 1d

Verifiable answers are essential. Mathematical proofs are ideal—wrong proofs don’t compile in Lean.

In domains without clear-cut verifiable truth, rely on consistency: within the conversation, with what you know, and with external independent sources.

1 1

iamwil @interjectedfuture.com · 1d

Genuine curiosity forces you to struggle with core concepts, not just accept AI’s answers.

It unearths hidden corners in your understanding, which makes for good questions to challenge the AI. It’s also motivation to keep going when you hit a wall.

1 1

iamwil @interjectedfuture.com · 1d

Critical thinking must be a habit of mind. Doubt the sycophantic agreement. Double-check assertions by clicking quoted sources and doing independent searches. If anything is incongruent, confusing, or missing—ask why.

1 1

iamwil @interjectedfuture.com · 1d

Adjacent domain expertise matters: AI hallucinates. It will say things that are slightly wrong or ill-informed.

Without expertise in a related field, those errors accumulate in your mental model. Despite the effort to learn, you can actively make yourself stupider.

1 3

iamwil @interjectedfuture.com · 1d

This isn't vibe coding. It requires:

1. Adjacent domain expertise (to catch AI errors)
2. Vigilant critical thinking (doubt everything)
3. Genuine curiosity (fuel for good questions)
4. Verifiable answers (domains where correctness is checkable)

1 4

iamwil @interjectedfuture.com · 1d

When syntax confused, ask contextually:

"What does this keyword mean in this proof?"
"Why did this tactic fail?"
"What are the tradeoffs between using ring vs simp?"

The answers come in context of the specific problem, not abstract theory.

1 4

iamwil @interjectedfuture.com · 1d

When unfamiliar concepts appeared, adjust the explanation:

"Explain this in terms a developer would understand"
"Why a function instead of a Map here?"
"Rewrite this Lean code in TypeScript so I can use it as a Rosetta Stone"

1 4

iamwil @interjectedfuture.com · 1d

The old path: Learn Lean (6 weeks), study abstract algebra (8 weeks), understand group theory (4 weeks), finally attempt your proof.

The new path: Start with your exact problem. Generate a tutorial for it. Backfill concepts as you hit them.

1 16

iamwil @interjectedfuture.com · 1d

I proved Z-sets form an abelian group in Lean—a formal verification of DBSP's merge operation—in one afternoon.

Not because I knew type theory or proof assistants. Because AI collapses the activation barrier.

interjectedfuture.com/the-best-wa...

The Best Way to Learn Might Be Starting at the End: Writing a Proof in Lean

AI leveraged learning lets you start with the application at the end. Curiosity guides what you learn, fundamentals backfill when you need them.

interjectedfuture.com

1 3

iamwil @interjectedfuture.com · 1d

New post: Most people think you need foundations before attempting hard things. Prerequisites as requirements.

But that's just an artifact of industrial-scale curriculum design. Prerequisites are activation energy, not gatekeepers. 🧵

2 1 13

iamwil @interjectedfuture.com · 1d

what happened?

1

iamwil @interjectedfuture.com · 3d

Learned a new word: "chiaroscuro"

Good for image prompting, I guess. I have yet to find a use for "erinaceous".

1

iamwil @interjectedfuture.com · 4d

It's the same debate going on when I was in school. I agree then as I do now: it's better for the students to learn the theory in school. Glad my school didn't bow to the pressure to teach Java in the classes.

x.com/GuptaAnkitV...

iamwil @interjectedfuture.com · 4d

We are a dynamic economy that uses capitalism to allocate resources. There were other more enticing industries with better margins and growth. This is both good and bad. We captured more of the future, but let our foundations rot.

x.com/Robotbeat/s...

1

iamwil @interjectedfuture.com · 6d

Globally unique identifier rundown:

DNS: Centralized coordination (ICANN) but fast
ENS: Decentralized consensus (blockchain) but slow
Local-first: No coordination (UUIDs) but ugly

2 4

iamwil @interjectedfuture.com · 6d

This is relatable, is from using vim and emacs, once I got into the habit of searching to navigate. However, that was only within the same document. Search across files was still painful without a plugin. One huge stream sounds like it's something easier to get used to.
x.com/alexobenaue...

1

iamwil @interjectedfuture.com · 7d

The juxtaposition of the fantastic with the mundane has always fascinated us. This sort of effect is even more pronounced in VR.

x.com/XRarchitect...

1 1

iamwil @interjectedfuture.com · 7d

Depends on the stage. I can only speak to the earlier stages. Strength of conviction. Living in the future. Protecting your optimism. Finding customers. Building good personal and organizational habits. Iterating quickly. The basics.