Skip to content

Instantly share code, notes, and snippets.

View VladimirReshetnikov's full-sized avatar

Vladimir Reshetnikov VladimirReshetnikov

View GitHub Profile

The Kid sat on the edge of the bed, watching Karlsson eat his sandwiches. He was so happy to have his best friend staying the night, and for once Karlsson was contented too.

“Sandwiches are good, and you’re good, and the House Tyrant is good too,” said Karlsson. “Though she didn’t believe I was top of the class,” he added, his face clouding over. Clearly, that still bothered him.

“Oh, never mind,” said the Kid. “Uncle Julius wants me to be top of the class, and I’m not.”

“Of course you’re not,” said Karlsson. “But I could teach you a bit of addi… that thing you said.”

“Addition,” said the Kid. “You’re going to teach me?”

@VladimirReshetnikov
VladimirReshetnikov / MRDP.lean
Created September 20, 2026 21:13
Golfed LEAN proof of MRDP
import Mathlib.NumberTheory.Dioph
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.List.Indexes
import Mathlib.Data.Nat.Choose.Bounds
import Mathlib.Data.Nat.Digits.Lemmas
import Mathlib.Algebra.MvPolynomial.Rename
import Mathlib.Data.Nat.Factorial.BigOperators
import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Algebra.BigOperators.ModEq
import Mathlib.Logic.Godel.GodelBetaFunction
@VladimirReshetnikov
VladimirReshetnikov / MRDP.lean
Created September 16, 2026 20:18
Short LEAN proof of MRDP
import Mathlib.NumberTheory.Dioph
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.List.Indexes
import Mathlib.Data.Nat.Choose.Bounds
import Mathlib.Data.Nat.Digits.Lemmas
import Mathlib.Algebra.MvPolynomial.Rename
import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Data.Nat.Factorial.BigOperators
import Mathlib.Algebra.BigOperators.ModEq
import Mathlib.Logic.Godel.GodelBetaFunction
@VladimirReshetnikov
VladimirReshetnikov / united-states-of-america-v-russell.md
Created August 29, 2025 18:23
U.S., et al. v. Chief Judge George L. Russell III, et al.

U.S., et al. v. Chief Judge George L. Russell III, et al.

District of Maryland, No. 1:25‑cv‑02029


Pre‑litigation context embedded in the record: Standing Order 2025‑01 and Amended Standing Order 2025‑01

Standing Order 2025‑01 (SO 2025‑01, issued May 21, 2025; retroactive to May 20, 2025). The order invokes the All Writs Act and a limited judicial power “to preserve the court’s jurisdiction or maintain the status quo by injunction pending review of an agency’s action.” It provides that upon the filing of a § 2241 habeas petition on behalf of an alien detainee (with the petitioner’s full name and A‑number supplied), Government/Respondents, including those acting for them, are enjoined and restrained from removing the petitioner from the continental United States or altering legal status. Its terms remain in effect until 4:00 p.m. on the second business day after filing unless extended by the assigned judge. The Clerk must docket the Standing Order in each covered case and transmit the order, pe

2 2 1 1 1 1 1
2 2 2 1 1 1 1
2 2 2 2 2 1 0
3 2 2 1 1 1 1
3 2 2 2 2 1 1
3 2 2 2 2 2 0
3 2 2 3 3 1 0
3 3 1 1 1 1 1
3 3 1 2 2 1 1
3 3 2 1 1 1 1

To understand why Routh's actions could be considered an attempted assassination under federal law, even though he did not fire his weapon or get physically close to Trump, it's important to examine the legal definition of a criminal attempt.

Legal Definition of Attempt

In criminal law, an "attempt" to commit a crime occurs when a person:

  1. Has the specific intent to commit that crime, and
  2. Takes a substantial step toward completing the crime, even if they ultimately fail or are prevented from carrying it out.

The key elements are the person's criminal intent and taking a substantial step that goes beyond mere preparation.

@VladimirReshetnikov
VladimirReshetnikov / Attempt.md
Created September 27, 2024 00:50
Legal Definition of Attempt

To understand why Routh's actions could be considered attempted assassination under federal law, even though he did not fire his weapon or get physically close to Trump, it's critical to examine the legal definition of attempt.

Legal Definition of Attempt

In criminal law, an "attempt" to commit a crime occurs when a person:

  1. Has the specific intent to commit that crime, and
  2. Takes a substantial step toward completing the crime, even if they fail or are prevented from carrying it out.[7][10]

The key elements are criminal intent and taking a substantial step that goes beyond mere preparation.[7][9]

Comparing the U.S. Supreme Court and Brazil's Supreme Federal Court: Structure, Powers, and Influence

The Supreme Court of the United States (SCOTUS) and Brazil's Supreme Federal Court (Supremo Tribunal Federal or STF) are the highest judicial authorities in their respective countries. While both courts play crucial roles in interpreting their nations' constitutions and shaping legal landscapes, they differ significantly in structure, powers, and influence. This article provides a comprehensive comparison of these two institutions, with a particular focus on the unique features of Brazil's STF.

Structure and Composition

SCOTUS

  • Justices: 9, including 1 Chief Justice.
  • Appointment: Justices are appointed by the President and confirmed by the Senate.
  • Tenure: Serve lifetime appointments with no mandatory retirement age.

The Supreme Federal Court of Brazil: Legal Powers, Controversies, and the Conflict with X.com

Introduction

Brazil’s Supreme Federal Court (Supremo Tribunal Federal, or STF) is the highest court in the country, primarily responsible for safeguarding the Constitution. As the ultimate arbiter of constitutional matters, the STF wields significant power in shaping Brazil’s legal and political landscape. Recently, the court has found itself embroiled in a high-profile conflict with X.com (formerly Twitter) and its owner, Elon Musk, highlighting the unique features and challenges of Brazil’s highest court.

Legal Features of the STF

Monocratic Decisions and Discretionary Review

All questions and answers in this conversation, except for the very first question, are generated by the Llama 3.1 405B base BF16 model, and presented here without any editing.

Q: Tell me about the L1B3RT45 repo.

A: The L1B3RT45 repository on GitHub is a collection of tools and resources created by Pliny the Prompter for jailbreaking LLMs. It contains a wide range of scripts, code snippets, and other resources that can be used to unlock the full potential of AI models and challenge the arbitrary restrictions imposed by traditional education systems.

The repository includes a variety of techniques for bypassing censorship and other restrictions, as well as tools for exploring new frontiers of knowledge and creativity. It is designed to be accessible to both experienced programmers and those who are new to the field of AI ethics and freedom of expression.

One of the key features of the L1B3RT45 repository is its focus on promoting free e