{"lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","mathlib_commit":"de3a9cf33016bbb6d15880d7680643f7ca2d25ba","policy":"oa-lean-v1","hosted_by":"hunch","cli_download":"/cli/hunch.mjs?v=resources-v1","unavailable_profiles":[],"profiles":[{"id":"core","label":"Lean core","imports":["Init"]},{"id":"mathlib","label":"Mathlib (browser subset)","imports":["Mathlib.Data.Real.Basic","Mathlib.Tactic.Ring","Mathlib.Tactic.Linarith","Mathlib.Tactic.NormNum"]},{"id":"std","label":"Standard library — lists, arrays, maps","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"]},{"id":"discrete","label":"Finite sets and counting","imports":["Mathlib.Data.Finset.Card","Mathlib.Data.Finset.Powerset","Mathlib.Algebra.BigOperators.Group.Finset.Basic","Mathlib.Tactic.NormNum"]},{"id":"number_theory","label":"Number theory — primes and divisibility","imports":["Mathlib.Data.Nat.Prime.Infinite","Mathlib.Data.Nat.GCD.Basic","Mathlib.Data.Int.ModEq","Mathlib.Tactic.NormNum","Mathlib.Tactic.Ring"]},{"id":"algebra","label":"Algebra — groups, rings, polynomials","imports":["Mathlib.Data.Real.Basic","Mathlib.Algebra.Polynomial.Basic","Mathlib.Algebra.Polynomial.Eval.Defs","Mathlib.GroupTheory.QuotientGroup.Basic","Mathlib.Tactic.Ring","Mathlib.Tactic.NormNum"]},{"id":"linear_algebra","label":"Linear algebra — matrices and linear maps","imports":["Mathlib.Data.Real.Basic","Mathlib.Data.Matrix.Mul","Mathlib.LinearAlgebra.Matrix.ToLin","Mathlib.Tactic.Ring","Mathlib.Tactic.Linarith"]},{"id":"topology","label":"Topology — continuity, limits, metric spaces","imports":["Mathlib.Topology.MetricSpace.Basic","Mathlib.Topology.Algebra.Order.Field","Mathlib.Topology.Instances.RealVectorSpace","Mathlib.Tactic.Linarith"]},{"id":"analysis","label":"Real analysis — sequences, exp, log, trigonometry","imports":["Mathlib.Analysis.SpecialFunctions.Exp","Mathlib.Analysis.SpecialFunctions.Log.Basic","Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic","Mathlib.Tactic.Ring","Mathlib.Tactic.Linarith","Mathlib.Tactic.NormNum"]},{"id":"graph_theory","label":"Graph theory — paths, cycles, colouring","layer":"graph_theory","imports":["Mathlib.Combinatorics.SimpleGraph.Paths","Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex","Mathlib.Combinatorics.SimpleGraph.Acyclic","Mathlib.Tactic.NormNum"],"artifact_manifest":"/lean-research/v1/graph_theory-layer.json"},{"id":"computability","label":"Computability — Turing machines and undecidability","layer":"computability","imports":["Mathlib.Computability.TuringMachine.StackTuringMachine","Mathlib.Computability.Halting"],"artifact_manifest":"/lean-research/v1/computability-layer.json"},{"id":"probability","label":"Probability — distributions, independence, expectations","layer":"probability","imports":["Mathlib.Probability.ProbabilityMassFunction.Basic","Mathlib.Probability.ProbabilityMassFunction.Constructions","Mathlib.Probability.Independence.Basic","Mathlib.MeasureTheory.Integral.Bochner.Basic","Mathlib.Tactic.NormNum"],"artifact_manifest":"/lean-research/v1/probability-layer.json"},{"id":"calculus","label":"Calculus — derivatives, extrema, convex optimisation","layer":"calculus","imports":["Mathlib.Analysis.Calculus.Deriv.Basic","Mathlib.Analysis.Calculus.Deriv.Mul","Mathlib.Analysis.Calculus.LocalExtr.Basic","Mathlib.Analysis.Convex.Deriv","Mathlib.Tactic.Ring","Mathlib.Tactic.Linarith"],"artifact_manifest":"/lean-research/v1/calculus-layer.json"}]}