{"entities":{"Q7361612":{"pageid":31520375,"ns":120,"title":"Item:Q7361612","lastrevid":105367706,"modified":"2026-10-07T13:37:15Z","type":"item","id":"Q7361612","labels":{"en":{"language":"en","value":"Unconstrained Optimization"}},"descriptions":{"en":{"language":"en","value":"AFP entry Unconstrained_Optimization"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e73b9752da1587ca6d28c8529598cfb6261f1da7","datavalue":{"value":"https://isa-afp.org/entries/Unconstrained_Optimization.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361612$DC3EEC2A-1DAA-4A7B-AA32-C30978AC70A0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"efad754626f161cd66c554302db22bd9c4d46e2c","datavalue":{"value":{"time":"+2025-07-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361612$A93A2BE4-6E47-401E-8065-A21D14771BD0","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0bf4d3ca5eedd1d75f040083aae2b975258503f7","datavalue":{"value":"Dustin Bryant","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361612$17805650-DAE9-46E9-87F4-CC9828F1B0FE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1d1562c63d91ceb91ef43656eaa5cde6de4f0dbe","datavalue":{"value":{"text":"Unconstrained Optimization","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361612$1F9976DA-4FCF-4A7D-B44E-8508EF2DF87F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a8967255b7700655bc632784646dd3f669627a55","datavalue":{"value":"As formal methods gain traction in machine learning and numerical analysis, the community needs computer-checked proofs of core optimization results. Existing Isabelle libraries still lack a foundational framework for unconstrained optimization. We close this gap with a comprehensive Isabelle/HOL development that formalizes: minimizers, strict and isolated local minimizers; first- and second-order optimality conditions for scalar functions \\( f : \\mathbb{R} \\to \\mathbb{R} \\); first-order optimality conditions for vector functions \\( g : \\mathbb{R}^{n} \\to \\mathbb{R} \\); and a worked example showing that the continuous function \\[ h(x) = \\begin{cases} x^{4} \\left( \\cos(1/x) + 2 \\right), & \\text{if } x \\neq 0, \\\\[4pt] 0, & \\text{if } x = 0 \\end{cases} \\] has a strict but non-isolated local minimizer at \\( x = 0 \\). The new session Unconstrained_Optimization provides sound, reusable foundations for future proof-checking tools and mechanized research in optimization, analysis, and algorithmic correctness.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361612$C75CB2DE-7CA8-4E2D-9DA2-B8A4EB218905","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361612$595223A3-40A2-4AED-893C-C84160A3AC27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914e8ee381069f563cdd221fe2896b0c7e646005","datavalue":{"value":{"entity-type":"item","numeric-id":5491447,"id":"Q5491447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361612$25CD5497-07A0-4102-84C2-D38A88AD9350","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361612$6B4E7899-3540-4723-835B-4F4CD8C7645D","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"026b4828839731a98542c5e0a4a583edfd8d6da5","datavalue":{"value":{"entity-type":"item","numeric-id":7361955,"id":"Q7361955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361612$FD1F8A3E-13AB-4224-B766-0EC33B619012","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"b04c93a3ee276587f8dc258d8de827d10d6ade60","datavalue":{"value":{"entity-type":"item","numeric-id":7360780,"id":"Q7360780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361612$78BA3F09-387A-4A8F-A932-8F9468BD354B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361612$BF23A544-BA94-40CE-B427-04D838B72197","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Unconstrained Optimization","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Unconstrained_Optimization"}}}}}