[SteveJS]

I am using lean as part of the prd.md description handed to a coding agent. The definitions in lean compile and mean exactly what I want them to say. The implementation i want to build is in rust.

HOWEVER … I hit something i now call a McLuhen vortex error: “When a tool, language, or abstraction smuggles in an implied purpose at odds with your intended goal.”

Using Lean implies to the coding agent ‘proven’ is a pervasive goal.

I want to use lean to be more articulate about the goal. Instead using lean smuggled in a difficult to remove implicit requirement that everything everywhere must be proven.

This was obvious because the definitions i made in lean imply the exact opposite of everything needs to be proven. When i use morphism i mean anything that is a morphism not only things proven to be morphisms.

A coding agent driven by an llm needs a huge amount of structure to use what the math says rather than take on the implications that because it is using a proof system therefore everything everywhere is better if proven.

The initial way i used lean poisoned the satisficing structure that unfolds during a coding pass.

[mycall]

Could you put that distinction into the AGENTS.md file so it will understand and follow that nuance?

[SteveJS]

I have several techniques queued up that attempt to counter it. The distinction in Agents.md is definitely part of it.

Not sure if they will work yet.