diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3493157..dde652c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Changelog
 
+## 0.1.1
+
+- Use LeanLink's environment evaluator and proof checks when available, while preserving compatibility with released LeanLink.
+- Prepare evaluation during module imports and share expression and proof cleanup.
+- Show expandable notebook summaries for sessions, declarations, values and expressions.
+- Read available installation output without unnecessary waits.
+
 ## 0.1.0
 
 - Add pinned mathlib installation and explicit Lean sessions.
diff --git a/MathlibLink/Kernel/Evaluate.wl b/MathlibLink/Kernel/Evaluate.wl
index 5334148..1e34ef7 100644
--- a/MathlibLink/Kernel/Evaluate.wl
+++ b/MathlibLink/Kernel/Evaluate.wl
@@ -10,6 +10,24 @@ Options[MathlibEvaluate] = {TimeConstraint -> 120, "ReturnType" -> Automatic}
 Options[MathlibCall] = Options[MathlibEvaluate]
 Options[ProveMathlib] = {TimeConstraint -> 120}
 
+MathlibExpression /: MakeBoxes[expression : MathlibExpression[_String], form : StandardForm | TraditionalForm] := mathlibExpressionBoxes[expression, form]
+
+(* Keep the released LeanLink usable while the environment interface is developed. *)
+importSource[state_Association, source_String] := If[mathlibDirectLeanQ[],
+	mathlibInvoke["LeanImportString", state["Environment"], source],
+	mathlibInvoke["LeanImportString", mathlibSessionSource[state] <> source, "ProjectDir" -> state["Directory"]]
+]
+
+verifyTheorem[term_, time_] := If[mathlibDirectLeanQ[],
+	mathlibInvoke["LeanVerify", term, "TimeLimit" -> time],
+	With[{axioms = term["Axioms"]},
+		If[! MatchQ[axioms, {___String}] || Complement[axioms, {"propext", "Quot.sound", "Classical.choice"}] =!= {},
+			mathlibFailure["UntrustedProof", "The theorem depends on an admitted proof or an additional axiom.", <|"Axioms" -> axioms|>],
+			TimeConstrained[term["KernelCheck"], time, $TimedOut]
+		]
+	]
+]
+
 mathlibQuoteName[name_String] := If[StringContainsQ[name, "\:00ab" | "\:00bb" | "\n" | "\r"],
 	mathlibFailure["MathlibUnsupportedName", "Use MathlibExpression for this Lean identifier."],
 	StringRiffle[("\:00ab" <> # <> "\:00bb" &) /@ StringSplit[name, ".", All], "."]
@@ -39,26 +57,32 @@ mathlibEncode[MathlibSession[sessionID_String], object_MathlibObject] := With[{d
 ]
 mathlibEncode[_, _] := mathlibFailure["MathlibUnsupportedValue", "Use an exact integer, rational, boolean, string, list, MathlibObject or MathlibExpression."]
 
-retainExpression[session_MathlibSession, state_Association, expression_String, time_] := Module[{name, source, environment, result},
-	name = "mathliblink_value_" <> StringDelete[CreateUUID[], "-"];
-	source = mathlibSessionSource[state] <> "noncomputable def " <> name <> " := (" <> expression <> ")\n";
-	environment = None;
+releaseEnvironment[environment_] := If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]],
+	mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]
+]
+
+elaborateSource[session_MathlibSession, state_Association, source_String, time_, failure_Failure] := Module[{environment = None, result},
 	result = CheckAbort[
-		TimeConstrained[environment = Quiet[Check[mathlibInvoke["LeanImportString", source, "ProjectDir" -> state["Directory"]], $Failed]], time, $TimedOut],
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
+		TimeConstrained[environment = Quiet[Check[importSource[state, source], $Failed]], time, $TimedOut],
+		releaseEnvironment[environment];
 		mathlibCloseSession[session]; Abort[]
 	];
 	If[result === $TimedOut,
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
+		releaseEnvironment[environment];
 		mathlibCloseSession[session];
 		Return[mathlibFailure["MathlibTimedOut", "Lean elaboration exceeded the time limit. The session was closed."]]
 	];
-	environment = result;
-	If[! MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]],
-		Return[mathlibFailure[If[environment === $TimedOut, "MathlibTimedOut", "MathlibElaborationFailed"], "Lean could not elaborate the expression.", <|"Expression" -> expression|>]]
-	];
+	If[MatchQ[result, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], result, failure]
+]
+
+retainExpression[session_MathlibSession, state_Association, expression_String, time_] := Module[{name, source, environment, result},
+	name = "mathliblink_value_" <> StringDelete[CreateUUID[], "-"];
+	source = "noncomputable def " <> name <> " := (" <> expression <> ")\n";
+	environment = elaborateSource[session, state, source, time,
+		mathlibFailure["MathlibElaborationFailed", "Lean could not elaborate the expression.", <|"Expression" -> expression|>]];
+	If[FailureQ[environment], Return[environment]];
 	result = mathlibKeepObject[session, environment[name], expression, environment];
-	If[FailureQ[result], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
+	If[FailureQ[result], releaseEnvironment[environment]];
 	result
 ]
 
@@ -70,7 +94,10 @@ MathlibEvaluate[session_MathlibSession, expression_String, opts : OptionsPattern
 	If[FailureQ[state], Return[state]];
 	If[mode === "Object", Return[retainExpression[session, state, expression, time]]];
 	result = CheckAbort[
-		mathlibInvoke["LeanEvaluate", expression, "ProjectDir" -> state["Directory"], "Imports" -> state["Imports"], "TimeLimit" -> time],
+		If[mathlibDirectLeanQ[],
+			mathlibInvoke["LeanEvaluate", state["Environment"], expression, "TimeLimit" -> time],
+			mathlibInvoke["LeanEvaluate", expression, "ProjectDir" -> state["Directory"], "Imports" -> state["Imports"], "TimeLimit" -> time]
+		],
 		mathlibCloseSession[session]; Abort[]
 	];
 	If[MatchQ[result, Failure["TimedOut", _]], mathlibCloseSession[session]];
@@ -91,7 +118,7 @@ MathlibCall[session_MathlibSession, name_String, arguments : Longest[Except[_Rul
 	]
 
 ProveMathlib[session_MathlibSession, statement_String, proof_String, opts : OptionsPattern[]] := Module[{
-	state, time, name, source, environment, term, axioms, checked, result, retained = False, started = AbsoluteTime[]
+	state, time, name, source, environment, term, checked, result, retained = False, started = AbsoluteTime[]
 },
 	If[! mathlibOptionsQ[ProveMathlib, {opts}], Return[mathlibFailure["MathlibInvalidOption", "Unknown proof option."]]];
 	time = OptionValue[TimeConstraint];
@@ -99,37 +126,22 @@ ProveMathlib[session_MathlibSession, statement_String, proof_String, opts : Opti
 	state = mathlibSessionData[session];
 	If[FailureQ[state], Return[state]];
 	name = "mathliblink_theorem_" <> StringDelete[CreateUUID[], "-"];
-	source = mathlibSessionSource[state] <> "theorem " <> name <> " : " <> statement <> " := " <> proof <> "\n";
-	environment = None;
-	result = CheckAbort[
-		TimeConstrained[environment = Quiet[Check[mathlibInvoke["LeanImportString", source, "ProjectDir" -> state["Directory"]], $Failed]], time, $TimedOut],
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
-		mathlibCloseSession[session]; Abort[]
-	];
-	If[result === $TimedOut,
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
-		mathlibCloseSession[session];
-		Return[mathlibFailure["MathlibTimedOut", "Lean elaboration exceeded the time limit. The session was closed."]]
-	];
-	environment = result;
-	If[! MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]],
-		Return[mathlibFailure[If[environment === $TimedOut, "MathlibTimedOut", "MathlibProofFailed"], "Lean did not produce the requested theorem.", <|"Statement" -> statement|>]]
-	];
+	source = "theorem " <> name <> " : " <> statement <> " := " <> proof <> "\n";
+	environment = elaborateSource[session, state, source, time,
+		mathlibFailure["MathlibProofFailed", "Lean did not produce the requested theorem.", <|"Statement" -> statement|>]];
+	If[FailureQ[environment], Return[environment]];
 	WithCleanup[
 		term = environment[name];
-		axioms = term["Axioms"];
-		If[! MatchQ[axioms, {___String}] || Complement[axioms, {"propext", "Quot.sound", "Classical.choice"}] =!= {},
-			Return[mathlibFailure["MathlibUntrustedProof", "The theorem depends on an admitted proof or an additional axiom.", <|"Axioms" -> axioms|>]]
-		];
 		checked = CheckAbort[
-			TimeConstrained[term["KernelCheck"], If[time === Infinity, Infinity, Max[0.001, time - (AbsoluteTime[] - started)]], $TimedOut],
+			verifyTheorem[term, If[time === Infinity, Infinity, Max[0.001, time - (AbsoluteTime[] - started)]]],
 			mathlibCloseSession[session]; Abort[]
 		];
-		If[checked === $TimedOut, mathlibCloseSession[session]; Return[mathlibFailure["MathlibTimedOut", "Kernel checking exceeded the time limit. The session was closed."]]];
+		If[checked === $TimedOut || MatchQ[checked, Failure["TimedOut", _]], mathlibCloseSession[session]; Return[mathlibFailure["MathlibTimedOut", "Kernel checking exceeded the time limit. The session was closed."]]];
+		If[MatchQ[checked, Failure["UntrustedProof", _]], Return[mathlibFailure["MathlibUntrustedProof", "The theorem depends on an admitted proof or an additional axiom.", <|"Axioms" -> checked["Axioms"]|>]]];
 		If[! MatchQ[checked, _Success], Return[mathlibFailure["MathlibKernelRejected", "Lean's kernel did not accept the theorem's module.", <|"Result" -> checked|>]]];
-		result = mathlibKeepObject[session, term, "((" <> proof <> ") : " <> statement <> ")", environment, True];
+		result = mathlibKeepObject[session, term, "((" <> proof <> ") : " <> statement <> ")", environment, True, statement];
 		retained = ! FailureQ[result];
 		result,
-		If[! retained, mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]]
+		If[! retained, releaseEnvironment[environment]]
 	]
 ]
diff --git a/MathlibLink/Kernel/Formatting.wl b/MathlibLink/Kernel/Formatting.wl
new file mode 100644
index 0000000..c47bf5d
--- /dev/null
+++ b/MathlibLink/Kernel/Formatting.wl
@@ -0,0 +1,58 @@
+PackageScoped[{mathlibSessionBoxes, mathlibObjectBoxes, mathlibExpressionBoxes}]
+
+(* Summaries use stored data only. Displaying an object must not evaluate Lean
+   code, query its native environment or repeat a proof check. *)
+
+summaryText[text_String] := Pane[Style[text, "Input", ShowStringCharacters -> False, TextAlignment -> Left],
+	ImageSize -> {{0, 480}, Automatic}, Alignment -> Left]
+
+summaryPreview[text_String] := With[{line = StringReplace[text, {"\r\n" -> " ", "\n" -> " ", "\r" -> " ", "\t" -> " "}]},
+	summaryText[If[StringLength[line] > 90, StringTake[line, 87] <> "...", line]]
+]
+
+summaryBox[head_, object_, items_List, details_List, form_] :=
+	BoxForm`ArrangeSummaryBox[head, object, None, items, details, form, "Interpretable" -> Automatic]
+
+mathlibSessionBoxes[session : MathlibSession[id_String], form_] :=
+	With[{state = Lookup[$mathlibSessions, id, <||>]},
+		summaryBox[MathlibSession, session,
+			{
+				BoxForm`SummaryItem[{"Status: ", Lookup[state, "Status", "Unavailable"]}],
+				If[KeyExistsQ[state, "DeclarationCount"], BoxForm`SummaryItem[{"Declarations: ", state["DeclarationCount"]}], Nothing]
+			},
+			{
+				If[KeyExistsQ[state, "Imports"], BoxForm`SummaryItem[{"Imports: ", Column[summaryText /@ state["Imports"]]}], Nothing],
+				If[KeyExistsQ[state, "Directory"], BoxForm`SummaryItem[{"Directory: ", summaryText[state["Directory"]]}], Nothing]
+			}, form]
+	]
+
+mathlibObjectBoxes[object : MathlibObject[id_String], form_] :=
+	Module[{data, state, term, kind, label, content},
+		data = Lookup[$mathlibObjects, id, <||>];
+		state = Lookup[$mathlibSessions, Lookup[data, "Session", ""], <||>];
+		If[Lookup[state, "Status", None] =!= "Ready",
+			Return[summaryBox[MathlibObject, object, {BoxForm`SummaryItem[{"Status: ", "Unavailable"}]}, {}, form]]
+		];
+		term = Replace[Lookup[data, "Term", None], {_[values_Association] :> values, _ -> <||>}];
+		kind = Which[
+			TrueQ[Lookup[data, "Verified", False]], "Checked theorem",
+			Lookup[data, "Environment", None] =!= None, "Typed expression",
+			True, Lookup[term, "Kind", "Declaration"]
+		];
+		{label, content} = Which[
+			StringQ[Lookup[data, "Statement", None]], {"Statement: ", data["Statement"]},
+			Lookup[data, "Environment", None] =!= None, {"Expression: ", Lookup[data, "Expression", ""]},
+			True, {"Name: ", Lookup[term, "Name", ""]}
+		];
+		summaryBox[MathlibObject, object,
+			{BoxForm`SummaryItem[{"Kind: ", kind}], BoxForm`SummaryItem[{label, summaryPreview[content]}]},
+			{
+				If[StringLength[content] > 90, BoxForm`SummaryItem[{label, summaryText[content]}], Nothing],
+				If[label =!= "Name: ", BoxForm`SummaryItem[{"Declaration: ", summaryText[Lookup[term, "Name", ""]]}], Nothing],
+				BoxForm`SummaryItem[{"Session: ", Lookup[state, "Status", "Unavailable"]}]
+			}, form]
+	]
+
+mathlibExpressionBoxes[expression : MathlibExpression[source_String], form_] :=
+	summaryBox[MathlibExpression, expression, {BoxForm`SummaryItem[{"Source: ", summaryPreview[source]}]},
+		{BoxForm`SummaryItem[{"Source: ", summaryText[source]}]}, form]
diff --git a/MathlibLink/Kernel/Installation.wl b/MathlibLink/Kernel/Installation.wl
index c56ab42..8616d6d 100644
--- a/MathlibLink/Kernel/Installation.wl
+++ b/MathlibLink/Kernel/Installation.wl
@@ -29,21 +29,27 @@ mathlibInstallStage[stage_String, fraction_ : None] := (
 
 (* Drain both pipes while polling, so a long cache download remains responsive.
    WithCleanup also stops the owned process on Throw, Abort or a callback error. *)
-mathlibInstallRun[arguments_List, directory_String, extraEnvironment_Association : <||>] := Module[{process, out = "", err = "", read},
+mathlibInstallRun[arguments_List, directory_String, extraEnvironment_Association : <||>] := Module[{process, out = "", err = "", read, stdout, stderr, newOut, newErr},
 	mathlibCheckCancellation[];
 	read[stream_] := Replace[ReadString[stream, EndOfBuffer], Except[_String] -> ""];
 	process = Quiet[Check[StartProcess[arguments, ProcessDirectory -> directory,
 		ProcessEnvironment -> mathlibEnvironment[extraEnvironment]], $Failed]];
 	If[! MatchQ[process, _ProcessObject], Return[$Failed]];
+	stdout = ProcessConnection[process, "StandardOutput"];
+	stderr = ProcessConnection[process, "StandardError"];
 	WithCleanup[
-		While[ProcessStatus[process] === "Running",
+		While[True,
 			mathlibCheckCancellation[];
-			out = out <> read[ProcessConnection[process, "StandardOutput"]];
-			err = err <> read[ProcessConnection[process, "StandardError"]];
-			Pause[0.1]
+			newOut = read[stdout];
+			newErr = read[stderr];
+			out = out <> newOut;
+			err = err <> newErr;
+			If[newOut === "" && newErr === "",
+				(* Output may remain buffered after the process exits. *)
+				If[ProcessStatus[process] =!= "Running", Break[]];
+				Pause[0.1]
+			]
 		];
-		out = out <> read[ProcessConnection[process, "StandardOutput"]];
-		err = err <> read[ProcessConnection[process, "StandardError"]];
 		mathlibCheckCancellation[];
 		<|"ExitCode" -> ProcessInformation[process, "ExitCode"], "StandardOutput" -> out, "StandardError" -> err|>,
 		If[ProcessStatus[process] === "Running", KillProcess[process]]
diff --git a/MathlibLink/Kernel/Internal/Common.wl b/MathlibLink/Kernel/Internal/Common.wl
index 0cd8792..583ab53 100644
--- a/MathlibLink/Kernel/Internal/Common.wl
+++ b/MathlibLink/Kernel/Internal/Common.wl
@@ -1,5 +1,9 @@
 PackageScoped[{mathlibFailure, mathlibLoadLean, mathlibInvoke, mathlibOptionsQ, mathlibTimeQ, mathlibModuleQ, mathlibDirectory, mathlibRuntime, mathlibExecutable, mathlibRun, mathlibVersionQ, mathlibLeanDirectory, mathlibBridgeReadyQ, mathlibElanHome, mathlibToolsDirectory, mathlibExecutables, mathlibPathDirectories, mathlibEnvironment}]
 
+PackageScoped[mathlibDirectLeanQ]
+
+mathlibDirectLeanQ[] := Names["Wolfram`LeanLink`LeanVerify"] =!= {} && With[{verify = Symbol["Wolfram`LeanLink`LeanVerify"]}, DownValues[verify] =!= {}]
+
 mathlibFailure[tag_String, message_String, data_Association : <||>] := Failure[tag, Join[<|"MessageTemplate" -> message|>, data]]
 
 mathlibRuntime[] := mathlibRuntime[] = Import[FileNameJoin[{PacletObject["WolframInstitute/MathlibLink"]["Location"], "Resources", "Runtime.json"}], "RawJSON"]
diff --git a/MathlibLink/Kernel/Object.wl b/MathlibLink/Kernel/Object.wl
index 7d5cc9c..53aabc1 100644
--- a/MathlibLink/Kernel/Object.wl
+++ b/MathlibLink/Kernel/Object.wl
@@ -6,11 +6,11 @@ MathlibDeclaration::usage = "MathlibDeclaration[session, name] gives a typed obj
 
 $mathlibObjects = <||>
 
-mathlibKeepObject[session : MathlibSession[sessionID_String], term_, expression_String, environment_ : None, verified_ : False] := Module[{id = CreateUUID[], state},
+mathlibKeepObject[session : MathlibSession[sessionID_String], term_, expression_String, environment_ : None, verified_ : False, statement_ : None] := Module[{id = CreateUUID[], state},
 	state = mathlibSessionData[session];
 	If[FailureQ[state], Return[state]];
 	AssociateTo[$mathlibObjects, id -> <|"Session" -> sessionID, "Term" -> term, "Expression" -> expression,
-		"Environment" -> environment, "Verified" -> verified|>];
+		"Environment" -> environment, "Verified" -> verified, "Statement" -> statement|>];
 	AssociateTo[$mathlibSessions, sessionID -> Append[state, "Objects" -> Append[state["Objects"], id]]];
 	MathlibObject[id]
 ]
@@ -67,13 +67,4 @@ MathlibDeclaration[session_MathlibSession, name_String] := With[{state = mathlib
 
 MathlibObject /: Normal[object_MathlibObject] := With[{data = mathlibObjectData[object]}, If[FailureQ[data], data, data["Term"]]]
 MathlibObject /: DeleteObject[MathlibObject[id_String]] := mathlibForgetObject[id]
-MathlibObject /: MakeBoxes[object : MathlibObject[id_String], form_] := With[{
-	data = Lookup[$mathlibObjects, id, None]
-}, With[{label = Which[
-	! AssociationQ[data], "Released",
-	TrueQ[data["Verified"]], "Checked theorem",
-	data["Environment"] =!= None, "Typed expression",
-	True, data["Term"]["Name"]
-]}, With[{boxes = ToBoxes[label, form]},
-	InterpretationBox[RowBox[{"MathlibObject", "[", boxes, "]"}], object]
-]]]
+MathlibObject /: MakeBoxes[object : MathlibObject[_String], form : StandardForm | TraditionalForm] := mathlibObjectBoxes[object, form]
diff --git a/MathlibLink/Kernel/Session.wl b/MathlibLink/Kernel/Session.wl
index 33701f9..7d85fad 100644
--- a/MathlibLink/Kernel/Session.wl
+++ b/MathlibLink/Kernel/Session.wl
@@ -20,9 +20,13 @@ StartMathlibSession[opts : OptionsPattern[]] := Module[{directory, imports, load
 	If[FailureQ[loaded], Return[loaded]];
 	imports = DeleteDuplicates[imports];
 	cacheKey = Hash[{directory, imports}, "SHA256", "HexString"];
+	If[KeyExistsQ[$mathlibEnvironments, cacheKey] && Information[$mathlibEnvironments[cacheKey]["Environment"], "Valid"] === False,
+		KeyDropFrom[$mathlibEnvironments, cacheKey]
+	];
 	If[KeyExistsQ[$mathlibEnvironments, cacheKey],
 		{environment, names} = Lookup[$mathlibEnvironments[cacheKey], {"Environment", "Names"}],
-		environment = Quiet[Check[mathlibInvoke["LeanImport", "ProjectDir" -> directory, "Imports" -> imports, "IncludeInternal" -> True], $Failed]];
+		environment = Quiet[Check[mathlibInvoke["LeanImport", "ProjectDir" -> directory, "Imports" -> imports, "IncludeInternal" -> True,
+			Sequence @@ FilterRules[{"PrepareEvaluation" -> True}, Options[Symbol["Wolfram`LeanLink`LeanImport"]]]], $Failed]];
 		If[! MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], Return[mathlibFailure["MathlibImportFailed", "Lean could not load the selected mathlib modules.", <|"Directory" -> directory, "Imports" -> imports|>]]];
 		names = Sort[Keys[environment]];
 		AssociateTo[$mathlibEnvironments, cacheKey -> <|"Environment" -> environment, "Names" -> names|>]
@@ -30,7 +34,7 @@ StartMathlibSession[opts : OptionsPattern[]] := Module[{directory, imports, load
 	session = MathlibSession[CreateUUID[]];
 	AssociateTo[$mathlibSessions, First[session] -> <|"Status" -> "Ready", "Directory" -> directory,
 		"Imports" -> DeleteDuplicates[imports], "Environment" -> environment, "Names" -> names, "Objects" -> {},
-		"DeclarationCount" -> Length[environment]|>];
+		"DeclarationCount" -> Length[environment], "CacheKey" -> cacheKey|>];
 	session
 ]
 
@@ -49,7 +53,10 @@ mathlibSessionSource[state_Association] := StringRiffle[("import " <> # &) /@ st
 mathlibCloseSession[session : MathlibSession[id_String]] := With[{state = Lookup[$mathlibSessions, id, None]},
 	If[AssociationQ[state] && state["Status"] === "Ready",
 		Scan[mathlibForgetObject, state["Objects"]];
-		AssociateTo[$mathlibSessions, id -> Append[KeyTake[state, {"Directory", "Imports", "DeclarationCount"}], "Status" -> "Closed"]]
+		AssociateTo[$mathlibSessions, id -> Append[KeyTake[state, {"Directory", "Imports", "DeclarationCount"}], "Status" -> "Closed"]];
+		If[mathlibDirectLeanQ[] && KeyExistsQ[state, "Environment"] && NoneTrue[Values[$mathlibSessions], Lookup[#, "Status", None] === "Ready" && Lookup[#, "CacheKey", None] === state["CacheKey"] &],
+			mathlibInvoke["LeanFreeEnvironment", state["Environment"], "EvaluatorOnly" -> True]
+		]
 	];
 	Null
 ]
@@ -60,9 +67,7 @@ mathlibCloseSession[session : MathlibSession[id_String]] := With[{state = Lookup
 (session_MathlibSession)[property_String] := Missing["UnknownProperty", property]
 
 MathlibSession /: DeleteObject[session_MathlibSession] := mathlibCloseSession[session]
-MathlibSession /: MakeBoxes[session : MathlibSession[id_String], form_] := With[{
-	status = Lookup[Lookup[$mathlibSessions, id, <||>], "Status", "Unavailable"]
-}, With[{boxes = ToBoxes[status, form]}, InterpretationBox[RowBox[{"MathlibSession", "[", boxes, "]"}], session]]]
+MathlibSession /: MakeBoxes[session : MathlibSession[_String], form : StandardForm | TraditionalForm] := mathlibSessionBoxes[session, form]
 
 MathlibNames[session_MathlibSession, pattern_String : "*"] := With[{state = mathlibSessionData[session]},
 	If[FailureQ[state], state, Select[state["Names"], StringMatchQ[#, pattern] &]]
diff --git a/MathlibLink/PacletInfo.wl b/MathlibLink/PacletInfo.wl
index 85356c7..d68c980 100644
--- a/MathlibLink/PacletInfo.wl
+++ b/MathlibLink/PacletInfo.wl
@@ -1,7 +1,7 @@
 PacletObject[<|
 	"Name" -> "WolframInstitute/MathlibLink",
 	"PublisherID" -> "WolframInstitute",
-	"Version" -> "0.1.0",
+	"Version" -> "0.1.1",
 	"WolframVersion" -> "15.0+",
 	"Description" -> "Connect Wolfram Language to mathlib for computation and checked proofs",
 	"Creator" -> "Wolfram Institute",
diff --git a/MathlibLink/ResourceDefinition.md b/MathlibLink/ResourceDefinition.md
index 4f64c3c..519f216 100644
--- a/MathlibLink/ResourceDefinition.md
+++ b/MathlibLink/ResourceDefinition.md
@@ -3,6 +3,7 @@ Template: Paclet
 ResourceType: Paclet
 Name: WolframInstitute/MathlibLink
 Context: WolframInstitute`MathlibLink`
+ContextPath: [Wolfram`LeanLink`]
 Paclet: WolframInstitute/MathlibLink
 Description: Connect Wolfram Language to mathlib for typed mathematics and checked proofs
 ContributedBy: Wolfram Institute
@@ -15,7 +16,7 @@ Categories: [Mathematics]
 
 ## Details & Options
 
-- Explicit sessions expose mathlib's complete imported declaration namespace.
+- MathlibLink prepares mathlib; LeanLink imports its complete declaration namespace.
 - Functions, theorems, structures and instances share a declaration interface.
 - Exact supported values can be copied to Wolfram Language; other expressions remain typed Lean objects.
 - Proof construction includes kernel replay and axiom checks.
@@ -24,20 +25,35 @@ Categories: [Mathematics]
 
 ## Usage
 
-[StartMathlibSession]() opens a session. [MathlibCall]() applies a named
-function, [MathlibDeclaration]() inspects a declaration, and [ProveMathlib]()
-checks a theorem. [InstallMathlib]() prepares the external runtime.
+[InstallMathlib]() prepares the runtime and [MathlibInstallation]() gives its
+project directory. Import that project with [LeanImport](paclet:Wolfram/LeanLink/ref/LeanImport),
+evaluate with [LeanEvaluate](paclet:Wolfram/LeanLink/ref/LeanEvaluate) and verify
+theorems with [LeanVerify](paclet:Wolfram/LeanLink/ref/LeanVerify).
+The environment interface requires the accompanying LeanLink development branch;
+existing MathlibLink session APIs remain supported.
 
 ## Basic Examples
 
+Import a focused mathlib module:
+
+```wl
+env = LeanImport["Mathlib.Data.Nat.Choose.Basic", "ProjectDir" -> MathlibInstallation[]["Directory"]]
+```
+
 Compute an exact binomial coefficient:
 
 ```wl
-WithCleanup[session = StartMathlibSession["Imports" -> {"Mathlib.Data.Nat.Choose.Basic"}], MathlibCall[session, "Nat.choose", 10, 4], DeleteObject[session]]
+LeanEvaluate[env["Nat.choose"], 10, 4]
+```
+
+Read a theorem's type:
+
+```wl
+env["Nat.add_comm"]["TypeForm"]
 ```
 
-Read a theorem from real analysis:
+Release the environment:
 
 ```wl
-WithCleanup[session = StartMathlibSession["Imports" -> {"Mathlib.Analysis.Complex.Exponential"}], MathlibDeclaration[session, "Real.exp_add"]["TypeForm"], DeleteObject[session]]
+LeanFreeEnvironment[env]
 ```
diff --git a/MathlibLink/Tests/Formatting.wlt b/MathlibLink/Tests/Formatting.wlt
new file mode 100644
index 0000000..27aac4c
--- /dev/null
+++ b/MathlibLink/Tests/Formatting.wlt
@@ -0,0 +1,46 @@
+Needs["WolframInstitute`MathlibLink`"]
+
+VerificationTest[
+	And @@ Flatten[Table[
+		With[{object = value}, ToExpression[ToBoxes[object, form], form, HoldComplete] === HoldComplete[object]],
+		{value, {MathlibSession["unknown"], MathlibObject["unknown"], MathlibExpression["(3 : Fin 5)"]}},
+		{form, {StandardForm, TraditionalForm}}
+	]], True, TestID -> "summary-copy-preserves-underlying-objects"
+]
+
+VerificationTest[
+	And @@ Table[
+		With[{object = value}, ToExpression[ToString[object, InputForm], InputForm, HoldComplete] === HoldComplete[object]],
+		{value, {MathlibSession["unknown"], MathlibObject["unknown"], MathlibExpression["\"a\\n\\\"b\" : String"]}}
+	], True, TestID -> "input-form-preserves-identifiers-and-source"
+]
+
+VerificationTest[
+	With[{object = MathlibExpression[StringRepeat[FromCharacterCode[945] <> " + ", 100] <> "0\n"]},
+		ToExpression[ToBoxes[object], StandardForm, HoldComplete] === HoldComplete[object]
+	], True, TestID -> "long-unicode-source-roundtrips-through-summary"
+]
+
+VerificationTest[
+	Module[{queries = 0, term, boxes},
+		term[_Association][_String] := (queries++; $Failed);
+		Block[{
+			WolframInstitute`MathlibLink`PackageScope`$mathlibSessions = <|"local" -> <|"Status" -> "Ready", "Imports" -> {"Mathlib"}, "Directory" -> "local", "DeclarationCount" -> 1|>|>,
+			WolframInstitute`MathlibLink`PackageScope`$mathlibObjects = <|"proof" -> <|"Session" -> "local", "Term" -> term[<|"Name" -> "example", "Kind" -> "theorem"|>], "Verified" -> True, "Statement" -> "forall n : Nat, n = n", "Environment" -> "owned"|>|>
+		},
+			boxes = ToBoxes /@ {MathlibSession["local"], MathlibObject["proof"]};
+			{queries, StringContainsQ[ToString[boxes, InputForm], "Checked theorem"], StringContainsQ[ToString[boxes, InputForm], "forall n : Nat, n = n"]}
+		]
+	], {0, True, True}, TestID -> "summary-uses-stored-metadata-without-querying-lean"
+]
+
+VerificationTest[
+	Block[{
+		WolframInstitute`MathlibLink`PackageScope`$mathlibSessions = <|"local" -> <|"Status" -> "Closed"|>|>,
+		WolframInstitute`MathlibLink`PackageScope`$mathlibObjects = <|"proof" -> <|"Session" -> "local", "Verified" -> True|>|>
+	},
+		With[{boxes = ToBoxes /@ {MathlibSession["local"], MathlibObject["proof"]}},
+			{StringContainsQ[ToString[boxes[[1]], InputForm], "Closed"], StringContainsQ[ToString[boxes[[2]], InputForm], "Unavailable"], ! StringContainsQ[ToString[boxes[[2]], InputForm], "Checked theorem"]}
+		]
+	], {True, True, True}, TestID -> "closed-session-does-not-display-live-proof"
+]
diff --git a/MathlibLink/Tests/Installation.wlt b/MathlibLink/Tests/Installation.wlt
index 44cbdbc..02eabf3 100644
--- a/MathlibLink/Tests/Installation.wlt
+++ b/MathlibLink/Tests/Installation.wlt
@@ -188,3 +188,15 @@ If[$OperatingSystem =!= "Windows",
 		TestID -> "installer-process-drains-both-streams-and-exit-status"
 	]
 ]
+
+If[$OperatingSystem =!= "Windows",
+	VerificationTest[
+		Module[{out = StringRepeat["o", 256], err = StringRepeat["e", 256], result},
+			result = WolframInstitute`MathlibLink`PackageScope`mathlibInstallRun[
+				{"/bin/sh", "-c", "i=0; while [ $i -lt 4096 ]; do printf '" <> out <>
+					"'; printf '" <> err <> "' >&2; i=$((i+1)); done; exit 7"}, Directory[]];
+			result === <|"ExitCode" -> 7, "StandardOutput" -> StringRepeat[out, 4096], "StandardError" -> StringRepeat[err, 4096]|>
+		],
+		True, TestID -> "installer-process-keeps-large-logs-on-both-streams"
+	]
+]
diff --git a/MathlibLink/Tests/Integration/Objects.wlt b/MathlibLink/Tests/Integration/Objects.wlt
index 3844ed4..29f13bc 100644
--- a/MathlibLink/Tests/Integration/Objects.wlt
+++ b/MathlibLink/Tests/Integration/Objects.wlt
@@ -10,7 +10,26 @@ VerificationTest[
 
 secondSession = StartMathlibSession["Imports" -> {"Mathlib.Analysis.Complex.Exponential"}];
 VerificationTest[MathlibCall[secondSession, "id", retained]["Tag"], "MathlibObjectSession", TestID -> "retained-object-session-boundary"]
+MathlibCall[session, "Nat.succ", 0];
+directLeanQ = Names["Wolfram`LeanLink`LeanVerify"] =!= {};
+If[directLeanQ,
+	sharedEnvironment = Wolfram`LeanLink`LeanImport["Mathlib.Analysis.Complex.Exponential", "ProjectDir" -> session["Directory"]];
+	sharedHandle = Information[sharedEnvironment, "Handle"];
+	sharedWorker = Wolfram`LeanLink`Private`$evaluationWorkers[sharedHandle]["Process"]
+];
 DeleteObject[session];
 VerificationTest[retained["TypeForm"]["Tag"], "MathlibInvalidObject", TestID -> "close-invalidates-owned-objects"]
 VerificationTest[MathlibCall[secondSession, "Nat.succ", 41], 42, TestID -> "closing-one-session-preserves-shared-environment"]
+If[directLeanQ,
+	VerificationTest[ProcessStatus[sharedWorker], "Running", TestID -> "shared-evaluator-survives-first-session-close"]
+];
 DeleteObject[secondSession];
+
+If[directLeanQ,
+	VerificationTest[ProcessStatus[sharedWorker], "Finished", TestID -> "last-session-close-stops-evaluator"];
+	VerificationTest[Information[sharedEnvironment, "Valid"], True, TestID -> "session-close-preserves-borrowed-lean-environment"];
+	Wolfram`LeanLink`LeanFreeEnvironment[sharedEnvironment];
+	reopened = StartMathlibSession["Imports" -> {"Mathlib.Analysis.Complex.Exponential"}];
+	VerificationTest[MathlibCall[reopened, "Nat.succ", 41], 42, TestID -> "session-reloads-explicitly-freed-environment"];
+	DeleteObject[reopened]
+];
diff --git a/MathlibLink/Tests/Integration/Values.wlt b/MathlibLink/Tests/Integration/Values.wlt
index 4f370ac..ba81b1a 100644
--- a/MathlibLink/Tests/Integration/Values.wlt
+++ b/MathlibLink/Tests/Integration/Values.wlt
@@ -2,6 +2,15 @@ Needs["WolframInstitute`MathlibLink`"]
 
 session = StartMathlibSession["Imports" -> {"Mathlib.Data.Nat.Sqrt", "Mathlib.Data.Nat.Totient", "Mathlib.Computability.PartrecCode"}];
 
+If[MemberQ[First /@ Options[Wolfram`LeanLink`LeanImport], "PrepareEvaluation"],
+	preparedEnvironment = Wolfram`LeanLink`LeanImport["ProjectDir" -> session["Directory"], "Imports" -> session["Imports"], "Filter" -> "Nat.sqrt"];
+	VerificationTest[
+		With[{worker = Wolfram`LeanLink`Private`$evaluationWorkers[Information[preparedEnvironment, "Handle"]]},
+			{ProcessStatus[worker["Process"]], KeyExistsQ[worker, "RequestID"]}],
+		{"Running", False}, TestID -> "session-prepares-evaluator-before-first-call"
+	]
+];
+
 VerificationTest[MathlibCall[session, "Nat.sqrt", 1000], 31, TestID -> "generic-integer-root-call"]
 VerificationTest[MathlibCall[session, "Nat.totient", 100], 40, TestID -> "generic-number-theory-call"]
 VerificationTest[MathlibEvaluate[session, "(2 : Nat) ^ 100"], 2^100, TestID -> "large-value-lossless"]
diff --git a/README.md b/README.md
index 8fad277..39c514b 100644
--- a/README.md
+++ b/README.md
@@ -4,8 +4,8 @@
 [![Release](https://github.com/WolframInstitute/MathlibLink/actions/workflows/release.yml/badge.svg)](https://github.com/WolframInstitute/MathlibLink/actions/workflows/release.yml)
 
 MathlibLink connects Wolfram Language to [mathlib](https://leanprover-community.github.io/mathlib4_docs/),
-Lean's mathematics library. It provides declaration lookup, typed objects,
-exact computations and checked proofs through explicit sessions.
+Lean's mathematics library. MathlibLink prepares the runtime; LeanLink imports
+its declarations, evaluates expressions and checks proofs.
 
 Requires Wolfram Language 15.0 or later.
 
@@ -19,6 +19,9 @@ Install and load the paclet:
 
 ```wl
 PacletInstall[ResourceObject["https://wolfr.am/1IuI3kKSs"]]
+```
+
+```wl
 Needs["WolframInstitute`MathlibLink`"]
 ```
 
@@ -32,45 +35,67 @@ Setup reuses working Git, curl and elan installations. See
 [InstallMathlib](https://www.wolframcloud.com/obj/wolframinstitute/MathlibLink/#ref/InstallMathlib) for setup
 options and progress reporting.
 
-Import binomial coefficients and compute a value:
+The environment interface below requires the accompanying LeanLink
+`feature/environment-evaluation` branch until its next release. Existing
+`StartMathlibSession`, `MathlibCall` and `ProveMathlib` calls remain supported.
+
+Load LeanLink:
 
 ```wl
-session = StartMathlibSession["Imports" -> {"Mathlib.Data.Nat.Choose.Basic"}]
-MathlibCall[session, "Nat.choose", 10, 4]
+Needs["Wolfram`LeanLink`"]
 ```
 
-Inspect a theorem:
+Import the binomial-coefficient module from the installed mathlib project:
+
+```wl
+env = LeanImport["Mathlib.Data.Nat.Choose.Basic", "ProjectDir" -> MathlibInstallation[]["Directory"], "PrepareEvaluation" -> True]
+```
+
+Apply an imported function:
+
+```wl
+LeanEvaluate[env["Nat.choose"], 10, 4]
+```
+
+Evaluate a family of inputs in one call:
+
+```wl
+LeanEvaluate[env, "(List.range 11).map (fun k => Nat.choose 10 k)"]
+```
+
+`"PrepareEvaluation" -> True` prepares the evaluator while importing modules.
+Later calls reuse it; `Needs` alone starts no Lean process.
+Batching inputs also reduces transfers between Wolfram Language and Lean.
+
+Compile a theorem using the same imports:
 
 ```wl
-MathlibDeclaration[session, "Nat.add_comm"]["TypeForm"]
+proofs = LeanImportString[env, "theorem addZero (n : Nat) : n + 0 = n := by rfl"]
 ```
 
-Prove an identity:
+Check its proof and axiom dependencies:
 
 ```wl
-proof = ProveMathlib[session, "∀ n : Nat, n + 0 = n", "by intro n; rfl"]
+LeanVerify[proofs["addZero"]]
 ```
 
-Close the session:
+Release the environments when finished:
 
 ```wl
-DeleteObject[session]
+Scan[LeanFreeEnvironment, {proofs, env}]
 ```
 
 ## Coverage
 
-The default session imports `Mathlib` and exposes its complete declaration
-namespace. Functions, theorems, structures and instances use the same lookup
-interface. There is no hand-maintained list of supported function names.
-Use `MathlibNames[session, "Nat.*"]` to browse names and
-`MathlibDeclaration[session, name]` to inspect a declaration.
-The [coverage report](docs/coverage.md) records the complete namespace check
-and live verification results.
+Use `LeanImport["Mathlib", "ProjectDir" -> directory]` for the full library,
+or select modules to reduce startup time and memory use. `Keys[env]` lists
+names; `env[name]` returns a Lean term whose type, definition and axioms can
+be inspected. No function whitelist or separate mathlib evaluator is needed.
 
 Computable expressions can produce Wolfram values. Noncomputable definitions
-and proofs remain typed Lean objects. A finite computation and a
-kernel-checked theorem establish different things; see
-[values and proofs](https://www.wolframcloud.com/obj/wolframinstitute/MathlibLink/#tutorial/ValuesAndProofs).
+and proofs remain typed Lean terms. See [values and proofs](docs/en/Tutorials/ValuesAndProofs.md)
+for examples, and the [coverage report](docs/coverage.md) for namespace and
+live verification results.
 
 ## Documentation
 
diff --git a/docs/architecture.md b/docs/architecture.md
index dd03f84..de4ca8b 100644
--- a/docs/architecture.md
+++ b/docs/architecture.md
@@ -1,17 +1,23 @@
 # Design
 
-MathlibLink connects Wolfram Language to the complete declaration namespace
-of a pinned mathlib release. It follows PARILink's explicit sessions,
-structured arguments, retained objects and error handling. It is independent
-of the applications that use it.
+MathlibLink prepares a pinned mathlib release for LeanLink. Normal use imports
+modules with LeanImport, inspects LeanTerms, evaluates with LeanEvaluate and
+checks theorems with LeanVerify. MathlibLink adds no separate evaluator or
+function whitelist. It remains independent of applications that use it.
 
-LeanLink supplies the native Lean environment, elaboration, evaluation and
-kernel-checking operations. MathlibLink supplies a reproducible mathlib setup,
-session-owned object lifetimes, generic calls, declaration discovery and
-upstream documentation links. There is no hand-maintained function whitelist.
-The default session imports Mathlib; smaller import lists reduce startup cost.
-Definitions, theorems, typeclasses and noncomputable declarations remain Lean
-objects when they cannot be copied as Wolfram values.
+LeanLink owns imported environments and their evaluation processes. A worker
+starts on the first evaluation, or during import with "PrepareEvaluation" -> True.
+Compatibility sessions enable this option for new imports when available.
+Later calls reuse that worker. Each request starts from the same imported environment, so temporary
+source declarations and errors do not affect subsequent requests. Computed
+values are not cached. Exact supported values cross the interface as JSON;
+noncomputable definitions and proofs remain LeanTerms.
+
+The environment interface is developed with LeanLink's
+feature/environment-evaluation branch. Released LeanLink versions remain
+usable through the existing MathlibLink session APIs. Those APIs are
+compatibility adapters: when the new interface is available, evaluation,
+source imports and strict proof verification delegate to LeanLink.
 
 Loading the paclet performs no installation or network access. InstallMathlib
 explicitly prepares elan, Git and curl when needed, then installs the pinned Lean
@@ -30,10 +36,13 @@ reset or overwritten. Interrupted setup can be rerun at the same revision.
 Sessions borrow LeanLink's cached import environments. Closing one session
 invalidates its objects without freeing another session's shared environment.
 Compiled expressions and proofs have unique environment handles, released when
-the owning object or session closes. Cached imported modules remain under LeanLink's
-ownership. Session and object identifiers are valid only in the creating kernel.
+the owning object or session closes. When the last compatibility session using an environment closes, its evaluator
+is stopped; the native environment stays valid for direct LeanLink users.
+A later call restarts evaluation as needed. Explicitly released environments
+are removed from the session import cache before reuse. Session and object
+identifiers are valid only in the creating kernel.
 
-LeanLink 1.2.5 also retains native imported-module regions until the kernel exits;
+LeanLink also retains native imported-module regions until the kernel exits;
 freeing an environment handle does not reclaim those regions. Its
 [environment loader](https://github.com/WolframInstitute/LeanLink/blob/8f9d43c5422b0514229a7fc3407a86b160f67423/Native/lib/LeanLink/EnvStore.lean#L49-L57)
 documents this lifetime. Prefer explicit module imports for focused work.
@@ -41,7 +50,7 @@ Independent live-test phases run in fresh Wolfram kernels so repeated full
 imports do not accumulate across the suite. Full-default namespace, call and
 proof checks remain part of the live tests.
 
-MathlibEvaluate runs Lean's evaluator and copies supported JSON values.
+MathlibEvaluate delegates evaluation to LeanLink and copies supported values.
 MathlibCall builds a Lean application from exact structured values and typed
 source arguments. Neither operation is a theorem prover. ReturnType "Object"
 elaborates and retains a typed Lean definition, including noncomputable terms.
@@ -62,7 +71,7 @@ claim that a theorem or noncomputable function can be evaluated numerically.
 PacletPage is the sole documentation and archive pipeline; publishing is a
 separate explicit action.
 
-Timeouts and interruptions close the owning session for every execution path,
+Compatibility-session timeouts and interruptions close the owning session,
 including retained expressions and proofs. LeanEvaluate bounds its subprocess.
 TimeConstrained around LeanLink elaboration and native kernel checking is a
 best-effort bound: an uninterruptible native call can return after the deadline.
diff --git a/docs/en/Guides/MathlibLink.md b/docs/en/Guides/MathlibLink.md
index da4d100..fbdb639 100644
--- a/docs/en/Guides/MathlibLink.md
+++ b/docs/en/Guides/MathlibLink.md
@@ -12,18 +12,34 @@ RelatedTutorials: [GettingStarted, ArithmeticPatterns, ValuesAndProofs, PartialC
 
 ## Abstract
 
-MathlibLink connects Wolfram Language to mathlib through explicit Lean sessions.
-The full declaration namespace is available for inspection, exact computation
-and proof construction. Noncomputable definitions and theorems remain typed
-Lean objects.
+MathlibLink prepares mathlib for use through LeanLink. Imported functions,
+theorems, structures and instances are available as Lean terms. Computable
+expressions return Wolfram values; noncomputable definitions remain typed terms.
+The environment interface requires the accompanying LeanLink development branch.
 
 ## Functions
 
-### Setup and sessions
+### Setup
 
 - `InstallMathlib` install the pinned Lean and mathlib runtime
-- `MathlibInstallation` inspect its status and versions
-- `StartMathlibSession` open a session with all of mathlib or selected imports
+- `MathlibInstallation` inspect its status, directory and versions
+
+### Working through LeanLink
+
+- [LeanImport](paclet:Wolfram/LeanLink/ref/LeanImport) import mathlib modules
+- [LeanEnvironment](paclet:Wolfram/LeanLink/ref/LeanEnvironment) hold their declarations
+- [LeanTerm](paclet:Wolfram/LeanLink/ref/LeanTerm) inspect a declaration's type, definition and axioms
+- [LeanEvaluate](paclet:Wolfram/LeanLink/ref/LeanEvaluate) evaluate expressions and apply imported functions
+- [LeanImportString](paclet:Wolfram/LeanLink/ref/LeanImportString) compile additional definitions and theorems
+- [LeanVerify](paclet:Wolfram/LeanLink/ref/LeanVerify) check a theorem in Lean's kernel and audit its axioms
+- [LeanFreeEnvironment](paclet:Wolfram/LeanLink/ref/LeanFreeEnvironment) release an environment and stop its evaluator
+
+### Compatibility sessions
+
+Existing session-based code remains supported, including with released LeanLink
+versions. With the new environment interface, these calls delegate to LeanLink.
+
+- `StartMathlibSession` open a compatibility session
 - `MathlibSession` represent the lifetime of a session and its objects
 
 ### Declarations and expressions
diff --git a/docs/en/ReferencePages/Symbols/MathlibExpression.md b/docs/en/ReferencePages/Symbols/MathlibExpression.md
index 9313809..a669264 100644
--- a/docs/en/ReferencePages/Symbols/MathlibExpression.md
+++ b/docs/en/ReferencePages/Symbols/MathlibExpression.md
@@ -20,6 +20,7 @@ RelatedTutorials: [ValuesAndProofs]
 - *source* is a Lean expression string.
 - Use this form for type annotations, functions, hypotheses or values without an automatic Wolfram conversion.
 - Constructing this expression does not run Lean. It is elaborated when used by [MathlibCall]().
+- The summary previews the source; expand it to read the complete expression.
 - An ordinary Wolfram string argument remains string data.
 
 ## Basic Examples
diff --git a/docs/en/ReferencePages/Symbols/MathlibObject.md b/docs/en/ReferencePages/Symbols/MathlibObject.md
index 34c2cce..f64ded4 100644
--- a/docs/en/ReferencePages/Symbols/MathlibObject.md
+++ b/docs/en/ReferencePages/Symbols/MathlibObject.md
@@ -21,6 +21,7 @@ RelatedTutorials: [ValuesAndProofs]
 - Properties include "Name", "Kind", "Type", "TypeForm", "Term", "TermForm", "Axioms", "KernelCheck", "Module" and "DocumentationURL".
 - "TypeForm" and "TermForm" use Lean's printer. "Type" and "Term" preserve the Lean expression structure.
 - "Verified" is True for a theorem produced by [ProveMathlib](). Inspecting a declaration alone does not perform a new proof check.
+- The expandable summary shows the declaration, expression or checked statement. Displaying it does not run Lean or repeat a proof check.
 - [Normal]() gives the underlying LeanLink term.
 - The object belongs to its originating session and cannot be passed to another session.
 - Closing the session invalidates its objects.
diff --git a/docs/en/ReferencePages/Symbols/MathlibSession.md b/docs/en/ReferencePages/Symbols/MathlibSession.md
index 5e509dd..8cdaf4a 100644
--- a/docs/en/ReferencePages/Symbols/MathlibSession.md
+++ b/docs/en/ReferencePages/Symbols/MathlibSession.md
@@ -22,6 +22,7 @@ RelatedTutorials: [GettingStarted]
 - `session["Directory"]` gives its runtime directory.
 - `session["Imports"]` gives its selected Lean modules.
 - `session["DeclarationCount"]` gives the number of available declarations.
+- The expandable summary shows the session state and declaration count, with its imports and directory under the opener.
 - [DeleteObject]() closes the session. Its retained [MathlibObject]() values then become unavailable.
 
 ## Basic Examples
diff --git a/docs/en/ReferencePages/Symbols/StartMathlibSession.md b/docs/en/ReferencePages/Symbols/StartMathlibSession.md
index 8c89e5f..12e2545 100644
--- a/docs/en/ReferencePages/Symbols/StartMathlibSession.md
+++ b/docs/en/ReferencePages/Symbols/StartMathlibSession.md
@@ -20,6 +20,7 @@ RelatedTutorials: [GettingStarted, ValuesAndProofs]
 - The result is a [MathlibSession]() object.
 - The default import is "Mathlib", exposing the full imported declaration namespace.
 - "Imports" selects smaller Lean modules and their dependencies, reducing startup time and memory use.
+- With LeanLink's environment evaluator, new imports prepare evaluation while loading the modules.
 - Setup must be completed with [InstallMathlib]() before opening a session.
 - [DeleteObject]() closes a session and invalidates its retained objects. Imported modules remain cached until the kernel exits.
 - A failure to open the selected runtime gives [Failure]().
diff --git a/docs/en/Tutorials/ArithmeticPatterns.md b/docs/en/Tutorials/ArithmeticPatterns.md
index 02dd421..c572f98 100644
--- a/docs/en/Tutorials/ArithmeticPatterns.md
+++ b/docs/en/Tutorials/ArithmeticPatterns.md
@@ -4,6 +4,7 @@ Name: ArithmeticPatterns
 Title: Exact Arithmetic Patterns
 Description: Compute binomial coefficients, common divisors and totients in Lean and plot the results
 Context: WolframInstitute`MathlibLink`
+ContextPath: [Wolfram`LeanLink`]
 Paclet: WolframInstitute/MathlibLink
 URI: WolframInstitute/MathlibLink/tutorial/ArithmeticPatterns
 Keywords: [exact arithmetic, binomial coefficients, greatest common divisor, totient]
@@ -18,13 +19,13 @@ with a Wolfram computation before plotting a larger pattern. Import the
 binomial-coefficient and totient modules used in this experiment:
 
 ```wl
-session = StartMathlibSession["Imports" -> {"Mathlib.Data.Nat.Choose.Basic", "Mathlib.Data.Nat.Totient"}]
+env = LeanImport["ProjectDir" -> MathlibInstallation[]["Directory"], "Imports" -> {"Mathlib.Data.Nat.Choose.Basic", "Mathlib.Data.Nat.Totient"}]
 ```
 
 Compute the coefficient in Lean:
 
 ```wl
-MathlibCall[session, "Nat.choose", 10, 4]
+LeanEvaluate[env["Nat.choose"], 10, 4]
 ```
 
 Compute it independently in Wolfram Language:
@@ -38,7 +39,7 @@ with the row coordinate increasing upward. The integer array is retained for
 comparison:
 
 ```wl
-ArrayPlot[Reverse[pascal = MathlibEvaluate[session, "(List.range 32).map (fun n => (List.range 32).map (fun k => Nat.choose n k % 2))"]], DataRange -> {{0, 31}, {0, 31}}, FrameTicks -> Automatic, FrameLabel -> {"Row n", "Column k"}]
+ArrayPlot[Reverse[pascal = LeanEvaluate[env, "(List.range 32).map (fun n => (List.range 32).map (fun k => Nat.choose n k % 2))"]], DataRange -> {{0, 31}, {0, 31}}, FrameTicks -> Automatic, FrameLabel -> {"Row n", "Column k"}]
 ```
 
 Check the entire finite array against the built-in binomial function:
@@ -57,7 +58,7 @@ Compute and display the greatest common divisor of each pair of integers
 from 1 to 32:
 
 ```wl
-ArrayPlot[MathlibEvaluate[session, "(List.range 32).map (fun n => (List.range 32).map (fun k => Nat.gcd (n + 1) (k + 1)))"], FrameTicks -> Automatic, FrameLabel -> {"First integer", "Second integer"}, PlotLegends -> Automatic]
+ArrayPlot[LeanEvaluate[env, "(List.range 32).map (fun n => (List.range 32).map (fun k => Nat.gcd (n + 1) (k + 1)))"], FrameTicks -> Automatic, FrameLabel -> {"First integer", "Second integer"}, PlotLegends -> Automatic]
 ```
 
 Large values occur at pairs sharing large divisors. The array is symmetric
@@ -65,7 +66,7 @@ because exchanging the two arguments preserves their greatest common divisor.
 Inspect the corresponding theorem:
 
 ```wl
-MathlibDeclaration[session, "Nat.gcd_comm"]["TypeForm"]
+env["Nat.gcd_comm"]["TypeForm"]
 ```
 
 ## Totients
@@ -74,7 +75,7 @@ Euler's totient counts the integers from 1 through n that are coprime to n.
 Compute the values for n from 1 through 64 and plot the count:
 
 ```wl
-ListPlot[totients = MathlibEvaluate[session, "(List.range 64).map (fun n => Nat.totient (n + 1))"], DataRange -> {1, 64}, AxesLabel -> {"n", "Totient"}]
+ListPlot[totients = LeanEvaluate[env, "(List.range 64).map (fun n => Nat.totient (n + 1))"], DataRange -> {1, 64}, AxesLabel -> {"n", "Totient"}]
 ```
 
 Compare the exact list with Wolfram Language's totient function:
@@ -87,8 +88,8 @@ The data remain ordinary exact integers after transfer. Wolfram plotting and
 analysis functions can use them without converting theorem statements or
 Lean's typeclass machinery.
 
-Close the session:
+Release the environment:
 
 ```wl
-DeleteObject[session]
+LeanFreeEnvironment[env]
 ```
diff --git a/docs/en/Tutorials/GettingStarted.md b/docs/en/Tutorials/GettingStarted.md
index 024d94a..6043b7e 100644
--- a/docs/en/Tutorials/GettingStarted.md
+++ b/docs/en/Tutorials/GettingStarted.md
@@ -2,117 +2,82 @@
 Template: TechNote
 Name: GettingStarted
 Title: Getting Started with MathlibLink
-Description: Open a mathlib session, find declarations and compute exact values
+Description: Import mathlib with LeanLink, inspect declarations and compute exact values
 Context: WolframInstitute`MathlibLink`
+ContextPath: [Wolfram`LeanLink`]
 Paclet: WolframInstitute/MathlibLink
 URI: WolframInstitute/MathlibLink/tutorial/GettingStarted
-Keywords: [mathlib, Lean, session, declarations]
+Keywords: [mathlib, Lean, imports, declarations]
 RelatedGuides: [MathlibLink]
 RelatedTutorials: [ArithmeticPatterns, ValuesAndProofs, PartialComputations]
 ---
 
-## Open a session
+## Import mathlib
 
 Mathlib contains definitions and theorems in algebra, analysis, geometry,
-number theory, topology and computability. MathlibLink uses one interface for
-the entire imported namespace. A declaration does not need a separate
-Wolfram wrapper before it can be inspected or used in a Lean expression.
+number theory, topology and computability. MathlibLink prepares its runtime;
+LeanLink supplies the same import, evaluation and proof operations used for
+other Lean projects. These examples require the environment interface in
+LeanLink's accompanying development branch.
 
-Install the pinned runtime once, if it is not already present. Setup reuses
-working Git, curl and elan installations and installs missing prerequisites in
-user directories:
+Install the pinned runtime once if needed:
 
 ```wl
 #| eval: false
 InstallMathlib[]
 ```
 
-Inspect the local installation:
+Find the prepared project:
 
 ```wl
-MathlibInstallation[]
+directory = MathlibInstallation[]["Directory"]
 ```
 
-The result separates overall readiness from the discovered tools.
-"Executables" gives the Elan, Lake, Git and Curl paths; "PathDirectories" gives
-the runtime directories to prepend when starting a child process.
-
-Open the full library:
+Import the modules used below:
 
 ```wl
-session = StartMathlibSession[]
+env = LeanImport["ProjectDir" -> directory, "Imports" -> {"Mathlib.Data.Nat.Sqrt", "Mathlib.Data.Nat.Choose.Basic"}]
 ```
 
-The default session exposes the whole library. For a focused computation,
-"Imports" can select smaller modules to reduce startup time and memory use;
-the following tutorials demonstrate this choice.
+Selected imports reduce startup time and memory use. To explore the entire
+library, use `"Imports" -> {"Mathlib"}` instead.
 
-## Find a declaration
+## Find and use a declaration
 
-Search for natural-number square-root declarations:
+Find natural-number square-root declarations:
 
 ```wl
-MathlibNames[session, "Nat.*sqrt*"]
+Select[Keys[env], StringMatchQ[#, "Nat.*sqrt*"] &]
 ```
 
-Inspect the square-root function:
+Read the square-root function's type:
 
 ```wl
-squareRoot = MathlibDeclaration[session, "Nat.sqrt"]
+env["Nat.sqrt"]["TypeForm"]
 ```
 
-Read its type:
+Compute the integer square root of 12345:
 
 ```wl
-squareRoot["TypeForm"]
+LeanEvaluate[env["Nat.sqrt"], 12345]
 ```
 
-Lean's `Nat` corresponds to exact nonnegative integers. Compute the integer
-square root of 12345:
-
-```wl
-MathlibCall[session, "Nat.sqrt", 12345]
-```
-
-Compare the result with a Wolfram computation:
+Compare with Wolfram Language:
 
 ```wl
 Floor[Sqrt[12345]]
 ```
 
-## Inspect a theorem
-
-The same declaration interface gives a theorem from real analysis:
-
-```wl
-exponentialLaw = MathlibDeclaration[session, "Real.exp_add"]
-```
-
-Read its quantified statement:
-
-```wl
-exponentialLaw["TypeForm"]
-```
-
-Find its upstream documentation:
-
-```wl
-Hyperlink["Exponential of a sum", exponentialLaw["DocumentationURL"]]
-```
-
-The installed runtime pins Lean 4.35.0 and mathlib v4.35.0. The linked
-[upstream reference](https://leanprover-community.github.io/mathlib4_docs/)
-tracks current mathlib; names or statements there can differ from the pinned
-runtime. The declaration's type in the active session is the one used by
-local computations and proofs.
+The evaluator starts on the first call and reuses the imports for later calls.
+Lean expressions and applications of imported terms use the same evaluator.
 
 ## Compute a family of values
 
-One Lean expression can produce an entire list. Compute binomial
-coefficients along row ten of Pascal's triangle:
+One Lean expression can return an entire list. Compute row ten of Pascal's
+triangle:
 
 ```wl
-row = MathlibEvaluate[session, "(List.range 11).map (fun k => Nat.choose 10 k)"]
+row = LeanEvaluate[env, "(List.range 11).map (fun k => Nat.choose 10 k)"]
 ```
 
 Plot the exact values:
@@ -121,18 +86,26 @@ Plot the exact values:
 ListPlot[row, DataRange -> {0, 10}, AxesLabel -> {"k", "Binomial coefficient"}]
 ```
 
-Inspect the continuity-of-composition theorem from topology:
+Batching related calculations reduces the number of transfers between the
+two languages. It does not change the mathematical algorithm.
+
+## Inspect a theorem
+
+Read a theorem's statement without evaluating it:
 
 ```wl
-MathlibDeclaration[session, "Continuous.comp"]["TypeForm"]
+env["Nat.add_comm"]["TypeForm"]
 ```
 
-The theorem remains accessible as a typed statement even though it is not a
-list-producing numerical computation. [Values and proofs](paclet:WolframInstitute/MathlibLink/tutorial/ValuesAndProofs)
-shows how these two uses fit together.
+[Values and proofs](paclet:WolframInstitute/MathlibLink/tutorial/ValuesAndProofs)
+shows how to add and verify a theorem using the same environment.
 
-Close the session after its last use:
+Release the imported environment and stop its evaluator:
 
 ```wl
-DeleteObject[session]
+LeanFreeEnvironment[env]
 ```
+
+The installed runtime pins Lean 4.35.0 and mathlib v4.35.0. The
+[upstream reference](https://leanprover-community.github.io/mathlib4_docs/)
+tracks current mathlib and may describe a newer version.
diff --git a/docs/en/Tutorials/PartialComputations.md b/docs/en/Tutorials/PartialComputations.md
index 6de5482..b8061bc 100644
--- a/docs/en/Tutorials/PartialComputations.md
+++ b/docs/en/Tutorials/PartialComputations.md
@@ -4,6 +4,7 @@ Name: PartialComputations
 Title: Observing Partial Computations
 Description: Inspect a formal computation model and compare bounded observations with its semantics
 Context: WolframInstitute`MathlibLink`
+ContextPath: [Wolfram`LeanLink`]
 Paclet: WolframInstitute/MathlibLink
 URI: WolframInstitute/MathlibLink/tutorial/PartialComputations
 Keywords: [computability, partial recursive functions, fuel, formal model]
@@ -23,13 +24,13 @@ connects codes to the partial-recursive function class.
 Import the partial-recursive code model:
 
 ```wl
-session = StartMathlibSession["Imports" -> {"Mathlib.Computability.PartrecCode"}]
+env = LeanImport["ProjectDir" -> MathlibInstallation[]["Directory"], "Imports" -> {"Mathlib.Computability.PartrecCode"}]
 ```
 
 Read its quantified statement:
 
 ```wl
-MathlibDeclaration[session, "Nat.Partrec.Code.exists_code"]["TypeForm"]
+env["Nat.Partrec.Code.exists_code"]["TypeForm"]
 ```
 
 The theorem gives a code for every function in the stated class. It does not
@@ -45,7 +46,7 @@ a count of Wolfram evaluation steps.
 Compose successor with itself and observe inputs 0 through 15 with fuel 20:
 
 ```wl
-MathlibEvaluate[session, "(List.range 16).map (fun n => Nat.Partrec.Code.evaln 20 (.comp .succ .succ) n)"]
+LeanEvaluate[env, "(List.range 16).map (fun n => Nat.Partrec.Code.evaln 20 (.comp .succ .succ) n)"]
 ```
 
 Measure which inputs finish as fuel increases from 1 through 20. Display
@@ -53,7 +54,7 @@ the completion map with increasing fuel to the right. Black cells mark a
 returned value; white cells mark an unfinished observation:
 
 ```wl
-ArrayPlot[Reverse[Transpose[Boole[finished = MathlibEvaluate[session, "(List.range 20).map (fun k => (List.range 16).map (fun n => (Nat.Partrec.Code.evaln (k + 1) (.comp .succ .succ) n).isSome))"]]]], DataRange -> {{1, 20}, {0, 15}}, FrameTicks -> Automatic, FrameLabel -> {"Input", "Fuel"}]
+ArrayPlot[Reverse[Transpose[Boole[finished = LeanEvaluate[env, "(List.range 20).map (fun k => (List.range 16).map (fun n => (Nat.Partrec.Code.evaln (k + 1) (.comp .succ .succ) n).isSome))"]]]], DataRange -> {{1, 20}, {0, 15}}, FrameTicks -> Automatic, FrameLabel -> {"Input", "Fuel"}]
 ```
 
 Count completed inputs at each fuel level:
@@ -72,13 +73,13 @@ Inspect the theorem that relates a returned bounded result to the partial
 semantics:
 
 ```wl
-MathlibDeclaration[session, "Nat.Partrec.Code.evaln_sound"]["TypeForm"]
+env["Nat.Partrec.Code.evaln_sound"]["TypeForm"]
 ```
 
 Inspect the converse statement for a computation that has a semantic result:
 
 ```wl
-MathlibDeclaration[session, "Nat.Partrec.Code.evaln_complete"]["TypeForm"]
+env["Nat.Partrec.Code.evaln_complete"]["TypeForm"]
 ```
 
 These declarations specify the connection between finite observations and the
@@ -86,8 +87,8 @@ formal semantics. A compiler targeting this model needs its own simulation
 proof before the model's computability results can be transferred to another
 language.
 
-Close the session:
+Release the environment:
 
 ```wl
-DeleteObject[session]
+LeanFreeEnvironment[env]
 ```
diff --git a/docs/en/Tutorials/ValuesAndProofs.md b/docs/en/Tutorials/ValuesAndProofs.md
index 86df57a..7156583 100644
--- a/docs/en/Tutorials/ValuesAndProofs.md
+++ b/docs/en/Tutorials/ValuesAndProofs.md
@@ -4,6 +4,7 @@ Name: ValuesAndProofs
 Title: Values, Types and Checked Proofs
 Description: Distinguish numerical evaluation, typed declarations and kernel-checked theorems
 Context: WolframInstitute`MathlibLink`
+ContextPath: [Wolfram`LeanLink`]
 Paclet: WolframInstitute/MathlibLink
 URI: WolframInstitute/MathlibLink/tutorial/ValuesAndProofs
 Keywords: [Lean, types, kernel, proof, noncomputable]
@@ -21,34 +22,40 @@ all inputs.
 Import the ring tactic for this identity:
 
 ```wl
-session = StartMathlibSession["Imports" -> {"Mathlib.Tactic.Ring"}]
+env = LeanImport["ProjectDir" -> MathlibInstallation[]["Directory"], "Imports" -> {"Mathlib.Tactic.Ring"}]
 ```
 
 Evaluate one natural-number identity:
 
 ```wl
-MathlibEvaluate[session, "decide ((4 + 1)^2 = (4 : Nat)^2 + 2*4 + 1)"]
+LeanEvaluate[env, "decide ((4 + 1)^2 = (4 : Nat)^2 + 2*4 + 1)"]
 ```
 
 Prove the polynomial identity for every integer:
 
 ```wl
-identity = ProveMathlib[session, "∀ x : Int, (x + 1)^2 = x^2 + 2*x + 1", "by intro x; ring"]
+proofs = LeanImportString[env, "theorem squareIdentity (x : Int) : (x + 1)^2 = x^2 + 2*x + 1 := by ring"]
+```
+
+Check the theorem in Lean's kernel and audit its axiom dependencies:
+
+```wl
+LeanVerify[proofs["squareIdentity"]]
 ```
 
 Read the theorem's complete type:
 
 ```wl
-identity["TypeForm"]
+proofs["squareIdentity"]["TypeForm"]
 ```
 
 Inspect its axiom dependencies:
 
 ```wl
-identity["Axioms"]
+proofs["squareIdentity"]["Axioms"]
 ```
 
-[ProveMathlib]() accepts the theorem after kernel replay and checks its axiom
+[LeanVerify](paclet:Wolfram/LeanLink/ref/LeanVerify) accepts the theorem after kernel replay and checks its axiom
 dependencies. The proof concerns the stated Lean proposition. It does not by
 itself establish the correctness of a separate Wolfram implementation.
 
@@ -56,13 +63,13 @@ The theorem `mul_comm` applies to a type with commutative multiplication.
 Inspect the type to see its algebraic assumptions:
 
 ```wl
-MathlibDeclaration[session, "mul_comm"]["TypeForm"]
+env["mul_comm"]["TypeForm"]
 ```
 
-Close this session before starting the next example:
+Release these environments:
 
 ```wl
-DeleteObject[session]
+Scan[LeanFreeEnvironment, {proofs, env}]
 ```
 
 ## Typed expressions without numerical evaluation
@@ -73,32 +80,32 @@ without an executable numerical implementation through Lean's evaluator.
 Import real square roots:
 
 ```wl
-session = StartMathlibSession["Imports" -> {"Mathlib.Analysis.Real.Sqrt"}]
+env = LeanImport["ProjectDir" -> MathlibInstallation[]["Directory"], "Imports" -> {"Mathlib.Analysis.Real.Sqrt"}]
 ```
 
 Retain the exact real square root of two:
 
 ```wl
-root = MathlibEvaluate[session, "Real.sqrt 2", "ReturnType" -> "Object"]
+roots = LeanImportString[env, "noncomputable def root : Real := Real.sqrt 2"]
 ```
 
 Read its type:
 
 ```wl
-root["TypeForm"]
+roots["root"]["TypeForm"]
 ```
 
 Inspect its defining expression:
 
 ```wl
-root["TermForm"]
+roots["root"]["TermForm"]
 ```
 
 Keeping the term does not replace it with a machine-precision approximation.
 Inspect mathlib's theorem for the square of a real square root:
 
 ```wl
-rootIdentity = MathlibDeclaration[session, "Real.sq_sqrt"]
+rootIdentity = env["Real.sq_sqrt"]
 ```
 
 Read its nonnegativity hypothesis and conclusion:
@@ -107,36 +114,40 @@ Read its nonnegativity hypothesis and conclusion:
 rootIdentity["TypeForm"]
 ```
 
-Close the square-root session:
+Release the square-root environments:
 
 ```wl
-DeleteObject[session]
+Scan[LeanFreeEnvironment, {roots, env}]
 ```
 
 Lean uses a theorem's type to infer its implicit arguments and typeclass
-instances. The scope example for [ProveMathlib]() checks an exponential law
-over real numbers using an existing mathlib theorem.
+instances. Existing mathlib theorems can be used in the source passed to
+[LeanImportString](paclet:Wolfram/LeanLink/ref/LeanImportString).
 
 ## Rejected admissions
 
 Lean's core module suffices for this example:
 
 ```wl
-session = StartMathlibSession["Imports" -> {"Init"}]
+env = LeanImport["ProjectDir" -> MathlibInstallation[]["Directory"], "Imports" -> {"Init"}]
 ```
 
 Lean source can contain `sorry`, which admits a proposition without supplying
 a proof. The proof interface rejects such a result:
 
 ```wl
-ProveMathlib[session, "False", "by sorry"]
+admitted = LeanImportString[env, "theorem admitted : False := by sorry"]
+```
+
+```wl
+LeanVerify[admitted["admitted"]]
 ```
 
 A timeout is also a failed observation, not evidence that the proposition is
 false. It may require a different proof or a larger resource budget.
 
-Close the session:
+Release these environments:
 
 ```wl
-DeleteObject[session]
+Scan[LeanFreeEnvironment, {admitted, env}]
 ```
diff --git a/docs/releases/0.1.1.md b/docs/releases/0.1.1.md
new file mode 100644
index 0000000..a73e2c7
--- /dev/null
+++ b/docs/releases/0.1.1.md
@@ -0,0 +1,12 @@
+# MathlibLink 0.1.1
+
+- Reuse LeanLink's imported environments for evaluation and proof checking when supported.
+- Prepare evaluation during imports, improve cleanup and remove unnecessary waits when reading installation output.
+- Display sessions, declarations, values and expressions as expandable notebook summaries.
+
+Existing MathlibLink session functions remain supported with LeanLink 1.2.5 or
+later. The new environment interface and evaluator preparation require
+[LeanLink PR #4](https://github.com/WolframInstitute/LeanLink/pull/4) until those
+changes are released. Loading MathlibLink does not start Lean or install software.
+
+Requires Wolfram Language 15.0 or later, Lean 4.35.0 and mathlib v4.35.0.
diff --git a/scripts/check.wls b/scripts/check.wls
index 194b1cc..b767aa7 100644
--- a/scripts/check.wls
+++ b/scripts/check.wls
@@ -13,6 +13,6 @@ coverage = AllTrue[symbols, Function[symbol, With[{name = Last[StringSplit[symbo
 ]]];
 usage = AllTrue[symbols, Function[symbol, StringQ[ToExpression[symbol <> "::usage"]]]];
 metadata = PacletObject[File[paclet]];
-valid = metadata["Name"] === "WolframInstitute/MathlibLink" && metadata["Version"] === "0.1.0";
+valid = metadata["Name"] === "WolframInstitute/MathlibLink" && metadata["Version"] === "0.1.1";
 Print[Length[files], " source/test files; ", Length[symbols], " public symbols."];
 Exit[If[syntax && coverage && usage && valid, 0, 1]];