Elektrine lite

← Feed

@carloangiuli@mathstodon.xyz

Post #1639301

2026-04-17 13:40 UTC

@maxsnew "formalising a textbook is arguably easier...because the answers to everything are in the text" uhhhh what

Replies (1)

  • @markusde@mathstodon.xyz 2026-04-17 14:21

    @carloangiuli @maxsnew didn't you know? Lean has a feature where you can formalize "exercise left for the reader" using `sorry`

    Open ##1639302