What problem does it solve? Legal arguments in Brazilian court decisions often hide structural defects: implicit premises, truncated warrants, internal contradictions, and omissions that are hard to distinguish from mere absent phrasing. This Skill formalizes arguments in Lean 4 so that every conclusion's exact dependency set becomes auditable via #print axioms, separating logical consequence from interpretive choice. ## Core Features & Use Cases - Formalization gate: Before writing any Lean, the Skill requires a concrete uncertainty the proof will reduce, and may conclude that formalization is not worth it. - Adversarial steelmanning: Reconstructs the challenged decision charitably with explicit STEEL_n premises, runs the mandatory art. 489 §1º III trivialness check, and audits which premises the court never actually stated. - Five-phase pipeline: Argdown argument mapping, Lean formalization with a six-layer architecture, independent substantive review, defeat synthesis with Mermaid graphs, and forensic translation back into conventional legal Portuguese. - Use Case: Given an appellate decision that invokes a binding precedent while ignoring its express caveat, use this Skill to model the ruling in Lean, prove that no legitimate response to the precedent was performed, and translate the finding into grounds for embargos de declaração. ## Quick Start Ask the agent to formalize this acórdão's argument in Lean 4 and show which precedents and facts each conclusion depends on.
