The claim. Let $c(n)$ be the maximum number of inclusion-minimal disconnecting vertex sets of a graph on $n$ vertices. The limit $\alpha=\lim_n c(n)^{1/n}$ exists (Proposition 2 with display (1)) and $\alpha\le2^{H(1/3)}<1.8899$ (Theorem 1), where $H$ is the binary entropy function (D. Bradač, On a question of Erdős and Nešetřil about minimal cuts in a graph, J. Graph Theory 108 (2025), no. 4, 817--818, published online 8 December 2024; arXiv:2409.02974, first posted 4 September 2024, whose v2 of 23 June 2026 is the version cited here). This answers Problem 150 in the affirmative: $c(n)^{1/n}\to\alpha$ for some $\alpha<2$.

The argument. Existence is proved for the marked-pair count $g(n)$, the largest number of minimal $(u,v)$-separators over graphs on $n+2$ vertices with marked $u,v$, which is supermultiplicative under merging, so Fekete's lemma applies; the paper then transfers the limit to $c(n)$ through the displayed sandwich $g(n-2)\le c(n)\le\binom n2g(n-2)$. The right inequality is immediate (a minimal cut is a minimal separator of any pair in different components); the left inequality is asserted as clear without an argument, and the problem page records it as a proof-coverage gap, not a dispute. The bound is an entropy count through $g(n)$ and display (1). Both proofs were read and followed, not checked line by line; the statements are paged at Theorem 1 and Proposition 2 of the source card.

Context. The arXiv v2 comment and the added note record that the bound was known earlier: Fomin, Kratsch, Todinca and Villanger (2008) proved $O(1.7087^n)$ minimal separators, the first proof that $\alpha<2$, and Fomin and Villanger (2012) and Gaspers and Mackenzie (2018) proved the golden ratio bound, all for minimal separators, which include the minimal cuts. Each is an accepted partial claim on the bound half of the question: Fomin, Kratsch, Todinca and Villanger, Fomin and Villanger and Gaspers and Mackenzie. The problem page records the lower bound $1.4457$ and the transfer of each bound through the same sandwich.

Acceptance. Refereed: Journal of Graph Theory, volume 108 (2025), issue 4, published online 8 December 2024 (the acknowledgment thanks the anonymous referee); the journal text was not compared with the arXiv version cited here. Reviewed: the site's curator, Thomas Bloom, credits this note with the first argument for the existence of the limit and with an independent proof of $\alpha<2$ in the problem's commentary (erdosproblems.com/150, last edited 21 June 2026, label PROVED (LEAN) since 31 March 2026).

Formalization, not evidence. The file Erdos150.lean of Boris Alexeev's repository lean-proofs at the pinned commit (linked above) declares itself a formalization of this note: its header names Bradač as informal author and Aristotle and Pietro Monticone as formal authors, and a thread post of 31 March 2026 by Monticone (linked above) reported the solution as autoformalized by the Aristotle system, with a link to an online type-checker. The file proves

limit_alpha_exists_and_lt_two : ∃ α, Tendsto (fun n ↦ (c n : ℝ) ^ (1 / n : ℝ)) atTop (nhds α) ∧ α < 2

with a comment that the theorem depends on the axioms propext, Classical.choice and Quot.sound; the formal-conjectures statement erdos_150 names it in its formal_proof attribute, and the site's label PROVED (LEAN) and the community database's Lean status date from the day of the post. Its IsMinCut G T is a minimal $(u,v)$-separator for some pair $u\ne v$, so its c n counts minimal separators, the quantity of the literature, not the problem's inclusion-minimal disconnecting sets: every minimal cut is a minimal separator and not conversely (the problem page's four-cycle with a pendant vertex), and the file does not address the left inequality of the sandwich that identifies the two growth rates. It has 1,298 lines and no occurrence of sorry, axiom, native_decide or unsafe; the corpus has not built, audited or kernel-checked it, and no outside review of it is known, so it is listed as a link and not as formalized evidence.