PythonPro #63: Python Mobile Wheels for iOS & Android, LLM 0.22 Updates, and Top Python Vizualization Tools 📊

Welcome to a brand new issue of PythonPro!

Here are today's News Highlights: PyPI now supports iOS and Android wheels for Python 3.13; LLM 0.22 adds API key support, a chatgpt-4o-latest alias, and logging improvements; llm-mlx enables running Apple MLX-optimized LLMs like Llama 3.2 3B on macOS.

My top 5 picks from today’s learning resources:

1. Top Python Data Visualization Libraries of 2025📊

2. How to Integrate Ollama and Deepseek-R1 with FastAPI for AI-Powered Chatbots🤖

3. Transforming Non-Stationary Time Series with Differencing🔄

4. The “late‐binding closure” pitfall in Python⚠️

5. 8 Open-Source AutoML Frameworks: How to Choose the Right One🤯

And, in From the Cutting Edge, we introduce FVAPPS, the largest formal verification benchmark, transforming coding interview problems into theorem-proving tasks in Lean 4, providing a rigorous test for AI models and researchers working on provably correct code generation.

Stay awesome!

Divya Anne Selvaraj

Editor-in-Chief

PS: We're conducting market research to better understand the evolving landscape of software engineering and architecture – including how professionals like you learn, grow and adapt to the impact of AI.

We think your insights would be incredibly valuable, and would love to hear what you have to say in a quick 1:1 conversation with our team.

What's in it for you?

✅ A brief 20–30 minute conversation at a time that’s convenient for you

✅ An opportunity to share your experiences and shape the future of learning

✅ A free credit to redeem any eBook of your choice from our library as a thank-you

How to Participate:

Schedule a quick call at your convenience using the link provided after the form:

https://forms.office.com/e/Bqc7gaDCKq

Looking forward to speaking with you soon!

Thank you,

Team Packt.

Note: Credits may take up to 15 working days to be applied to your account

Sign Up | Advertise

🐍 Python in the Tech 💻 Jungle 🌳

🗞️News

• PyPI Now Supports iOS and Android Wheels for Mobile Python Development: This follows PEP 730 (iOS support) and PEP 738 (Android support), both targeting Tier 3 support in Python 3.13.

• LLM 0.22, the annotated release notes: The version introduces API key support for models, a new chatgpt-4o-latest alias, improved logging and model search functionality, an embedding --prepend option, and various bug fixes.

• Run LLMs on macOS using llm-mlx and Apple’s MLX framework: llm-mlx, a new plugin for the LLM Python library and CLI, enables local execution of Apple MLX-optimized LLMs and simplifies running models like Llama 3.2 3B.

💼Case Studies and Experiments🔬

• URL-addressable Pyodide Python environments: Explores Datasette Lite, a browser-based Python environment powered by Pyodide and WebAssembly, highlighting its ability to run Python entirely in the browser.

• Lines, Scribbles, and an Algorithm: AI in Brain Mapping: Applies machine learning to classify EEG data, tests a model, analyzes its accuracy, and discusses broader implications.

📊Analysis

• A year of uv: pros, cons, and should you migrate: Explains uv’s advantages over traditional tools like pip and venv, when not to use it, and how Astral’s development approach ensures reliability and future improvements.

• Top Python Data Visualization Libraries of 2025: pygwalker leads as a low-code tool, matplotlib remains foundational with GPU support, and Plotly dominates dashboards. Seaborn, Bokeh, and Altair cater to statistical, streaming, and academic needs.

🎓 Tutorials and Guides 🤓

• Hermione's Undetectable Extension Charm: Revealed (Using Python): Uses Hermione's magical handbag from Harry Potter to explain Python's memory model, how references work, and why lists and other data structures appear to contain large objects while remaining small themselves.

• Transforming Non-Stationary Time Series with Differencing: Explains how differencing transforms non-stationary time series by removing trends, using first and second-order differencing, and applies this method to global temperature anomalies to prepare data for statistical modeling.

• Solving Markov Decision Processes with Value Iteration: Explains key MDP components, implements Bellman Equations for decision-making, and compares Value Iteration and Policy Iteration for optimizing movement strategies.

• How to Integrate Ollama and Deepseek-R1 with FastAPI for AI-Powered Chatbots: Provides step-by-step instructions to build an AI-powered chatbot, including setup, coding, API development, testing, and next steps.

• 3D DMD and Visualization with OpenFOAM and Python: Provides a step-by-step guide to applying 3D DMD to OpenFOAM computational fluid dynamics (CFD) simulations, using Python and ParaView.

• Quick Start Robotics and Reinforcement Learning with MuJoCo: Covers the library's core structure, MJCF format, integration with reinforcement learning algorithms such as PPO, and environment setup for training robotic agents in a simulated physics environment.

• Creating a private, custom distilled Deepseek-R1 model on your local machine & using it within an operational Python pipeline: Covers using Ollama and integrating it into a Python pipeline for AI-driven text analysis while ensuring data privacy and offline functionality.

🔑Best Practices and Advice🔏

• The “late‐binding closure” pitfall in Python: Explains how closures in Python capture variables by reference, not value, and provides a practical workaround to ensure expected behavior when using closures inside loops.

• Python Tooling Guide (Evergreen): Provides an up-to-date overview of the best tools for managing dependencies, linting, formatting, type checking, and editing as of early 2025.

• 8 Open-Source AutoML Frameworks: How to Choose the Right One: Covers early projects like Auto-WEKA and TPOT, widely used tools like Auto-sklearn and H2O AutoML, and modern frameworks like AutoGluon, FLAML, and PyCaret.

• Python Setup Tips: Recommends uv as the modern 2025 approach for speed and ease of use but includes Conda as an alternative; provides step-by-step instructions for installing Python, creating virtual environments, and managing dependencies.

• #TechForNewbies: Inheritance: Explains inheritance in OOP using a family analogy, demonstrating how child classes inherit properties and methods from parent classes, the difference between single and multiple inheritance, and how to manage conflicts in variable names.

🔍From the Cutting Edge: FVAPPS -- A Benchmark for Formally Verified Code Generation💥

In "Proving the Coding Interview: A Benchmark for Formally Verified Code Generation," Dougherty and Mehta introduce Formally Verified Automated Programming Progress Standards (FVAPPS), the largest formal verification benchmark to date, containing 4,715 samples, including 1,083 curated ones. This benchmark expands upon Automated Programming Progress Standards (APPS), integrating interactive theorem proving into coding interview-style problems.

Context

Formal verification mathematically proves a program’s correctness, offering stronger assurances than traditional software testing. This is crucial in safety-critical applications such as medical devices, cybersecurity, and autonomous systems. While Large Language Models (LLMs) have improved in code generation, ensuring their correctness remains a challenge. FVAPPS provides a rigorous benchmark to evaluate both program synthesis and theorem proving.

Key Findings

• Largest Formal Verification Benchmark: FVAPPS converts APPS coding problems into 4,715 theorem-proving tasks using Lean 4.

• Structured Benchmark: Problems are provided as Lean 4 theorems with "sorry" placeholders, requiring formal proofs for correctness.

• Automated Dataset Generation: Uses Anthropic’s Claude Sonnet 3.5 for iterative improvements and verification.

• Baseline Model Performance:

  • Sonnet 3.5: Proved 30% of the attempted theorems.

  • Gemini 1.5: Proved 18% of the attempted theorems.

• Human vs AI Performance: A human spent 10 hours on a single problem but couldn't complete the proof, highlighting the challenge of formal verification.

What This Means for You

FVAPPS is valuable for AI researchers advancing formal verification and program synthesis, software engineers working on provably correct systems, Machine Learning developers refining AI theorem-proving capabilities, and hiring platforms assessing candidates using verifiable coding tasks.

Examining the Details

FVAPPS extends APPS by reformatting problems into theorem-proving tasks in Lean 4. The dataset undergoes a multi-stage process:

1. Data Processing: Extracts coding problems, consolidates unit tests, and reformulates solutions.

2. Lean Conversion: Converts Python solutions into function definitions and theorem statements with "sorry" placeholders.

3. Validation: Uses Lean’s type-checking system to verify theorem structures.

4. Quality Assurance: Ensures problems pass unit tests and align with formal verification principles.

5. Curation: Filters out invalid or trivial problems, categorizing them into three subsets: unguarded (full dataset), guarded (unit test-verified), and guarded & plausible (most rigorous).

You can learn more by reading the entire paper or accessing FVAPPS.

And that’s a wrap.

We have an entire range of newsletters with focused content for tech pros. Subscribe to the ones you find the most useful here. The complete PythonPro archives can be found here.

If you have any suggestions or feedback, or would like us to find you a Python learning resource on a particular subject, just leave a comment below!